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 554  dedlem0b 759  meredith 921  nicodraw 949  19.21t 1111  a4imt 1154  ssuni 2512  omordi 4181  omsmolem 4240  r1ord 4627  aceq5 4712  aceq6a 4713  alephordi 4846  suppsr3 5196  nnsub 5903  monoord 6231  ser1add2 6275  ser1add 6276  seq1bnd 6847  cau3ir 6852  cvg2 6859  caubnd 6863  caure 6864  cauim 6865  facdivt 6879  facwordit 6881  clm4le 7019  2climnn 7039  2climnn0 7040  climsqueeze 7076  climsqueeze2 7077  climabslem 7084  caucvglem4 7096  cvgcmp3c 7122  infpnlem1 7449  islp2 7688  metcnss2 7838  lmuni 7886  caussi 7889  lmfexlem3 7893  metcnp4lem2 7903  xplmi 7907  xplm 7909  iscms2lem3 7925  iscms2lem4 7926  bcthlem18 7950  minveclem25 8500  minveclem26 8501  occllem6 9094  projlem25 9126  osumlem4 9498  nlelch 9909  hmopidmch 9990  mdsymlem6 10243  homcard 10426

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

Copyright terms: Public domain