Theorem anim2d 559

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

Hypothesis

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

Assertion

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

Proof of Theorem anim2d

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anbi2d 614  equvini 1164  moeq3 1912  ssel 2053  sscon 2161  uniss 2511  trel3 2678  ssopab2 2811  dfwe2 2925  ssrel 3237  fununi 3549  imadif 3560  ssimaex 3753  tfrlem1 3896  ss2ixp 4338  xpdom2 4422  infsdomnn 4511  unfi2 4529  unifi2 4533  inf3lem1 4585  zfregs 4619  cfub 4880  cflim 4881  distrlem2pr 5100  ltexprlem3 5116  suppsr2 5195  pre-axsup 5263  nnunb 6017  xrsupsslem 6023  xrinfmsslem 6024  supxr 6028  qbtwnxr 6217  qsqueeze 6218  iooss2 6311  indstr 6393  fzss2t 6436  bccl2t 6909  fsumcom 6966  fsumrev 6967  fsummulc1 6971  climmulc2 7065  cvgratlem2ALT 7183  cvgratlem2 7186  infxpidmlem7 7501  tgclt 7566  tgss2t 7579  neips 7668  ssnei2 7671  cnpco 7708  metreslem 7762  opnuni 7808  neibl 7817  metcnp 7826  metcnss2 7838  lmcau 7930  sspmval 8326  sspival 8331  ubthlem6 8465  shmods 9277  atcvat4 10232  cdj3lem2b 10269

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