Theorem 3anim123i 823

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

This theorem is referenced by:  syl3an 870  syl3anl 878  cla43egv 1869  eloprabg 4014  distrlem3pr 5148  le2tri3 5608  divasst 5755  lemul1t 5841  nnleltp1t 5963  elioo4g 6393  elfz2nn0t 6503  expord2t 6612  cvgratlem2ALT 7255  cvgratlem2 7258  metxplem4 7837  hcau2 9057  cm2jt 9565  irredlem2 10321  nnssi2 10422  nnssi3 10423  elo 10447  infi1 10449  cnvhmph 10521  filintf 10562  infi 10567  rcfpfillem4 10574  eqidob 10702

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 779

Copyright terms: Public domain