Theorem 3anim123i 821

Description: Join antecedents and consequents with conjunction.

Hypotheses

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

Assertion

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

Proof of Theorem 3anim123i

Step	Hyp	Ref	Expression
1		3anim123i.1	. . . 4 |- (ph -> ps)
2		3anim123i.2	. . . 4 |- (ch -> th)
3	1, 2	anim12i 333	. . 3 |- ((ph /\ ch) -> (ps /\ th))
4		3anim123i.3	. . 3 |- (ta -> et)
5	3, 4	anim12i 333	. 2 |- (((ph /\ ch) /\ ta) -> ((ps /\ th) /\ et))
6		df-3an 777	. 2 |- ((ph /\ ch /\ ta) <-> ((ph /\ ch) /\ ta))
7		df-3an 777	. 2 |- ((ps /\ th /\ et) <-> ((ps /\ th) /\ et))
8	5, 6, 7	3imtr4 219	1 |- ((ph /\ ch /\ ta) -> (ps /\ th /\ et))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  syl3an 868  syl3anl 876  cla43egv 1866  eloprabg 4007  distrlem3pr 5129  le2tri3 5589  divasst 5741  lemul1t 5832  nnleltp1t 5954  elioo4g 6385  elfz2nn0t 6495  expord2t 6604  cvgratlem2ALT 7248  cvgratlem2 7251  metxplem4 7833  hcau2 9055  cm2jt 9563  irredlem2 10318  nnssi2 10419  nnssi3 10420  elo 10444  infi1 10447  infi1OLD 10448  cnvhmph 10527  filintf 10569  infi 10578  infiOLD 10579  rcfpfillem4 10591  rcfpfillem4OLD 10592  eqidob 10723

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain