Theorem anim1d 432

Description: Add a conjunct to right of antecedent and consequent in a deduction.

Hypothesis

Ref	Expression
anim1d.1	|- (ph -> (ps -> ch))

Assertion

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

Proof of Theorem anim1d

Step	Hyp	Ref	Expression
1		anim1d.1	. 2 |- (ph -> (ps -> ch))
2		idd 11	. 2 |- (ph -> (th -> th))
3	1, 2	anim12d 431	1 |- (ph -> ((ps /\ th) -> (ch /\ th)))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  eqvin.l1 851  del43 856  r19.27av 1293  reuss 1577  reupick 1578  ssdif 1600  ssrin 1661  iunss1 2002  po3nr 2136  frss 2173  cores 2659  fununi 2705  oaass 3163  ssnn 3429  fiint 3445  ac6s 3577  reclem2pr 3951  infxpidmlem7 4939  shorth 5176  shless 5348

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

metamath.org