Theorem anim2d 563

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anbi2d 618  equvini 1170  moeq3 1924  ssel 2066  sscon 2174  uniss 2525  trel3 2693  ssopab2 2828  dfwe2 2941  ssrel 3253  fununi 3569  imadif 3580  ssimaex 3774  tfrlem1 3917  ss2ixp 4360  xpdom2 4448  infsdomnn 4541  unfi2 4565  unfi2OLD 4566  unifi2OLD 4571  inf3lem1 4622  zfregs 4657  cfub 4920  cflim 4921  distrlem2pr 5140  ltexprlem3 5156  suppsr2 5235  pre-axsup 5303  nnunb 6072  xrsupsslem 6078  xrinfmsslem 6079  supxr 6083  qbtwnxr 6280  qsqueeze 6281  iooss2 6375  ioojoint 6417  indstr 6462  fzss2t 6505  bccl2t 6971  fsumcom 7028  fsumrev 7029  fsummulc1 7033  climmulc2 7129  cvgratlem2ALT 7248  cvgratlem2 7251  infxpidmlem7 7559  tgclt 7623  tgss2t 7636  neips 7724  ssnei2 7727  cnpco 7766  metreslem 7819  opnuni 7865  neibl 7874  metcnp 7884  metcnss2 7896  lmcau 7993  sspmval 8388  sspival 8393  ubthlem6 8530  shmods 9357  atcvat4 10319  cdj3lem2b 10359

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