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  6564  smores  6567  issubmnd  13814  issubg2m  14051  issubrng2  14627  issubrg2  14658  rnglidlmsgrp  14943  rnglidlrng  14944  issubassa3  15121  sslm  15473