Theorem imim2d 25

Description: Deduction adding nested antecedents.

Hypothesis

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

Assertion

Ref	Expression
imim2d	|- (ph -> ((th -> ps) -> (th -> ch)))

Proof of Theorem imim2d

Step	Hyp	Ref	Expression
1		imim2d.1	. . 3 |- (ph -> (ps -> ch))
2	1	a1d 12	. 2 |- (ph -> (th -> (ps -> ch)))
3	2	a2d 13	1 |- (ph -> ((th -> ps) -> (th -> ch)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syld 27  imim12d 29  anc2l 298  anc2r 299  pm5.31 358  prth 559  dedlem0b 766  meredith 931  nic-ax 969  nic-axALT 970  19.21t 1151  a4imt 1195  ssuni 2589  omordi 4333  omsmolem 4396  r1ord 4801  aceq5 4886  aceq6a 4887  alephordi 5024  suppsr3 5378  nnsubi 6102  monoord 6482  ser1add2i 6703  ser1addi 6704  seq1bndi 7113  cau3iri 7118  cvg2i 7125  caubndi 7129  caurei 7130  cauimi 7131  facdiv 7145  facwordi 7147  clm4lei 7284  2climnn 7305  2climnn0 7306  climsqueeze 7343  climsqueeze2 7344  climabslem 7351  caucvglem4 7363  cvgcmp3ci 7390  infpnlem1 7718  islp2 7957  metcnss2 8110  lmuni 8162  caussi 8165  lmfexlem3 8169  metcnp4lem2 8180  xplmi 8184  xplm 8186  iscms2lem3 8202  iscms2lem4 8203  bcthlem18 8227  minveclem25 8829  minveclem26 8830  occllem6 9454  projlem25 9486  osumlem4 9859  nlelchi 10273  hmopidmchi 10359  mdsymlem6 10617  homcard 11045  finsschain 11425  ordtypelem6 11432  omsubsdomlem2 11441  elomsubsd 11446  omsubinit 11451  lfinpfin 11574  filssufil 11656  fcluscf 11724  fcluscnplem 11729  rrncms 12075

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain