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 556  dedlem0b 761  meredith 924  nicodraw 952  19.21t 1115  a4imt 1158  ssuni 2522  omordi 4197  omsmolem 4256  r1ord 4655  aceq5 4740  aceq6a 4741  alephordi 4874  suppsr3 5224  nnsub 5956  monoord 6294  ser1add2 6338  ser1add 6339  seq1bnd 6910  cau3ir 6915  cvg2 6922  caubnd 6926  caure 6927  cauim 6928  facdivt 6942  facwordit 6944  clm4le 7081  2climnn 7102  2climnn0 7103  climsqueeze 7140  climsqueeze2 7141  climabslem 7148  caucvglem4 7160  cvgcmp3c 7186  infpnlem1 7506  islp2 7747  metcnss2 7899  lmuni 7951  caussi 7954  lmfexlem3 7958  metcnp4lem2 7969  xplmi 7973  xplm 7975  iscms2lem3 7991  iscms2lem4 7992  bcthlem18 8016  minveclem25 8569  minveclem26 8570  occllem6 9178  projlem25 9210  osumlem4 9581  nlelch 9994  hmopidmch 10079  mdsymlem6 10335  homcard 10539

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

Copyright terms: Public domain