Theorem anim1d 560

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm3.45 562  equvini 1168  r19.27av 1754  ssrexv 2115  ssdif 2172  reupick 2279  iunss1 2574  po3nr 2848  mouniss 2890  frss 2921  cores 3499  fununi 3563  oaass 4195  oarec 4196  ssnnfi 4535  ssnnfiOLD 4536  fiint 4559  fiintOLD 4560  ac6s 4756  reclem2pr 5157  qbtwnxr 6279  iooss1 6373  icoshft 6408  ioojoint 6416  fzoptht 6502  fzss1t 6503  fsumsplit 7020  climmullem5 7124  cncffvrn 7273  infpn2 7509  infxpidmlem7 7558  neiss 7723  cnpco 7769  metelcls 7965  shorth 9168  shless 9347

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