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 300  anc2r 301  pm5.31 360  prth 555  dedlem0b 760  meredith 923  nicodraw 951  19.21t 1114  a4imt 1157  ssuni 2518  omordi 4190  omsmolem 4249  r1ord 4638  aceq5 4723  aceq6a 4724  alephordi 4857  suppsr3 5207  nnsub 5913  monoord 6244  ser1add2 6288  ser1add 6289  seq1bnd 6862  cau3ir 6867  cvg2 6874  caubnd 6878  caure 6879  cauim 6880  facdivt 6894  facwordit 6896  clm4le 7034  2climnn 7055  2climnn0 7056  climsqueeze 7093  climsqueeze2 7094  climabslem 7101  caucvglem4 7113  cvgcmp3c 7139  infpnlem1 7466  islp2 7707  metcnss2 7861  lmuni 7913  caussi 7916  lmfexlem3 7920  metcnp4lem2 7931  xplmi 7935  xplm 7937  iscms2lem3 7953  iscms2lem4 7954  bcthlem18 7978  minveclem25 8528  minveclem26 8529  occllem6 9133  projlem25 9165  osumlem4 9538  nlelch 9950  hmopidmch 10035  mdsymlem6 10291  homcard 10485

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

Copyright terms: Public domain