Theorem im3an 605

Description: Join antecedents and consequents with conjunction.

Hypotheses

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

Assertion

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

Proof of Theorem im3an

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

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  syl3an 628  eloprabg 3035  distrlem3pr 3923  divasst 4239  le2tri3 4311  nnleltp1t 4448  atcvatlem 5770

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org