This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imim21b

Description: Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Wolf Lammen, 14-Sep-2013)

Ref Expression
Assertion imim21b 
|- ( ( ps -> ph ) -> ( ( ( ph -> ch ) -> ( ps -> th ) ) <-> ( ps -> ( ch -> th ) ) ) )

Proof

Step Hyp Ref Expression
1 bi2.04 
 |-  ( ( ( ph -> ch ) -> ( ps -> th ) ) <-> ( ps -> ( ( ph -> ch ) -> th ) ) )
2 pm5.5 
 |-  ( ph -> ( ( ph -> ch ) <-> ch ) )
3 2 imbi1d 
 |-  ( ph -> ( ( ( ph -> ch ) -> th ) <-> ( ch -> th ) ) )
4 3 imim2i 
 |-  ( ( ps -> ph ) -> ( ps -> ( ( ( ph -> ch ) -> th ) <-> ( ch -> th ) ) ) )
5 4 pm5.74d 
 |-  ( ( ps -> ph ) -> ( ( ps -> ( ( ph -> ch ) -> th ) ) <-> ( ps -> ( ch -> th ) ) ) )
6 1 5 bitrid 
 |-  ( ( ps -> ph ) -> ( ( ( ph -> ch ) -> ( ps -> th ) ) <-> ( ps -> ( ch -> th ) ) ) )