Theorem 3anim123d 1360

Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)

Hypotheses

Ref	Expression
3anim123d.1	|- ( ph -> ( ps -> ch ) )
3anim123d.2	|- ( ph -> ( th -> ta ) )
3anim123d.3	|- ( ph -> ( et -> ze ) )

Assertion

Ref	Expression
3anim123d	|- ( ph -> ( ( ps /\ th /\ et ) -> ( ch /\ ta /\ ze ) ) )

Proof of Theorem 3anim123d

Step	Hyp	Ref	Expression
1		3anim123d.1	. . . 4 |- ( ph -> ( ps -> ch ) )
2		3anim123d.2	. . . 4 |- ( ph -> ( th -> ta ) )
3	1, 2	anim12d 335	. . 3 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )
4		3anim123d.3	. . 3 |- ( ph -> ( et -> ze ) )
5	3, 4	anim12d 335	. 2 |- ( ph -> ( ( ( ps /\ th ) /\ et ) -> ( ( ch /\ ta ) /\ ze ) ) )
6		df-3an 1011	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 1011	. 2 |- ( ( ch /\ ta /\ ze ) <-> ( ( ch /\ ta ) /\ ze ) )
8	5, 6, 7	3imtr4g 205	1 |- ( ph -> ( ( ps /\ th /\ et ) -> ( ch /\ ta /\ ze ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  hb3and  1543  pofun  4459  soss  4461  wessep  4727  isopolem  6031  isosolem  6033  issmo2  6565  smores  6568  issubmnd  13813  issubg2m  14050  issubrng2  14626  issubrg2  14657  rnglidlmsgrp  14942  rnglidlrng  14943  issubassa3  15120  sslm  15490