Theorem anim12d 546

Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)

Hypotheses

Ref	Expression
anim12d.1	|- (ph -> (ps -> ch))
anim12d.2	|- (ph -> (th -> ta))

Assertion

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

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 |- (ph -> (ps -> ch))
2		anim12d.2	. 2 |- (ph -> (th -> ta))
3		idd 21	. 2 |- (ph -> ((ch /\ ta) -> (ch /\ ta)))
4	1, 2, 3	syl2and 469	1 |- (ph -> ((ps /\ th) -> (ch /\ ta)))

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anim1d  547  anim2d  548  prth  554  im2anan9  808  anim12dan  810  3anim123d  1259  2euswap  2280  ssunsn2  3866  leltfintr  4459  ltfintr  4460  xp11  5057  2elresin  5195  fun  5237  dff13  5472  isotr  5496  enmap2lem4  6067  enmap1lem4  6073  nnltp1c  6263  nchoicelem17  6306  fnfrec  6321