Theorem anim1d 562

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 61	. 2 |- (ph -> (th -> th))
3	1, 2	anim12d 560	1 |- (ph -> ((ps /\ th) -> (ch /\ th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm3.45 564  equvini 1170  r19.27av 1757  ssrexv 2118  ssdif 2175  reupick 2282  iunss1 2578  po3nr 2854  mouniss 2896  frss 2927  cores 3505  fununi 3569  oaass 4201  oarec 4202  ssnnfi 4545  ssnnfiOLD 4546  fiint 4572  fiintOLD 4573  ac6s 4766  reclem2pr 5169  qbtwnxr 6280  iooss1 6374  icoshft 6409  ioojoint 6417  fzoptht 6503  fzss1t 6504  fsumsplit 7020  climmullem5 7124  cncffvrn 7273  infpn2 7510  infxpidmlem7 7559  neiss 7720  cnpco 7766  metelcls 7962  shorth 9163  shless 9342

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

Copyright terms: Public domain