Theorem anim2d 561

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anbi2d 616  equvini 1168  moeq3 1921  ssel 2063  sscon 2171  uniss 2521  trel3 2688  ssopab2 2822  dfwe2 2935  ssrel 3247  fununi 3563  imadif 3574  ssimaex 3768  tfrlem1 3911  ss2ixp 4354  xpdom2 4442  infsdomnn 4532  unfi2 4553  unifi2 4558  inf3lem1 4613  zfregs 4647  cfub 4908  cflim 4909  distrlem2pr 5128  ltexprlem3 5144  suppsr2 5223  pre-axsup 5291  nnunb 6070  xrsupsslem 6076  xrinfmsslem 6077  supxr 6081  qbtwnxr 6279  qsqueeze 6280  iooss2 6374  ioojoint 6416  indstr 6461  fzss2t 6504  bccl2t 6971  fsumcom 7028  fsumrev 7029  fsummulc1 7033  climmulc2 7129  cvgratlem2ALT 7248  cvgratlem2 7251  infxpidmlem7 7558  tgclt 7624  tgss2t 7637  neips 7727  ssnei2 7730  cnpco 7769  metreslem 7822  opnuni 7868  neibl 7877  metcnp 7887  metcnss2 7899  lmcau 7996  sspmval 8392  sspival 8397  ubthlem6 8534  shmods 9362  atcvat4 10324  cdj3lem2b 10364

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