Theorem anim1d 559

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 557	1 |- (ph -> ((ps /\ th) -> (ch /\ th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm3.45 561  equvini 1166  r19.27av 1751  ssrexv 2111  ssdif 2168  reupick 2275  iunss1 2569  po3nr 2843  mouniss 2885  frss 2916  cores 3491  fununi 3555  oaass 4185  oarec 4186  ssnn 4520  fiint 4540  ac6s 4736  reclem2pr 5137  qbtwnxr 6225  iooss1 6318  icoshft 6349  fzoptht 6442  fzss1t 6443  fsumsplit 6966  climmullem5 7068  cncffvrn 7216  infpn2 7460  infxpidmlem7 7509  neiss 7673  cnpco 7719  metelcls 7916  shorth 9107  shless 9285

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