Theorem 3anim123i 819

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 775	. 2 |- ((ph /\ ch /\ ta) <-> ((ph /\ ch) /\ ta))
7		df-3an 775	. 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 773

This theorem is referenced by:  syl3an 866  syl3anl 873  cla43egv 1857  eloprabg 3992  distrlem3pr 5101  le2tri3 5563  divasst 5704  lemul1t 5788  nnleltp1t 5901  elioo4g 6318  elfz2nn0t 6427  expord2t 6535  cvgratlem2ALT 7183  cvgratlem2 7186  metxplem4 7773  hcau2 8976  cm2jt 9480  irredlem2 10226  elo 10345  infi1 10347  cnvhmph 10414  filintf 10443  infi 10448  eqidob 10567

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 775

Copyright terms: Public domain