Theorem mpid 58

Description: A nested modus ponens deduction.

Hypotheses

Ref	Expression
mpid.1	|- (ph -> ch)
mpid.2	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
mpid	|- (ph -> (ps -> th))

Proof of Theorem mpid

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 |- (ph -> ch)
2	1	a1d 15	. 2 |- (ph -> (ps -> ch))
3		mpid.2	. 2 |- (ph -> (ps -> (ch -> th)))
4	2, 3	mpdd 57	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.43a 80  mpan2d 766  reuuniss2 3817  peano5 3975  reiotass2 5111  oeordi 5262  ordtypelem6 5689  omsubinit 5890  prlem936 6307  negeui 6510  receui 6890  caubndi 8178  clm4lei 8341  climcaui 8416  caucvglem2 8418  cvgratlem1ALT 8509  cvgratlem1 8512  cvgratlem4 8515  uniopn 8867  islp2 9023  metxplem4 9110  lmle 9238  metelcls 9243  metcnp4 9248  grpid 9349  blocnilem 9804  minveclem27 9916  fiiu2 10220  nmcopexlem6 11593  nmcfnexlem6 11622  hmopidmchi 11723  dmdbr3 11877  dmdbr4 11878  atom1d 11925  dfon2lem8 13856  infi1 14343  fiiu 14344  prltub 14602  grpdivone 14736  osneisi 14875  hmeogrp 14892  top2ind 14897  prtoptop 14919  cnfilca 14927  tarsuc2 15245  isseg1 15304  mtord 15346  finsschain 15373  ordtypelem6OLD 15380  omsubinitOLD 15399  cncls 15419  cnntr 15420  uncomp 15433  hscptsscld 15434  lfinpfin 15513  comppfsc 15517  ist1-2 15542  isufil2 15565  filssufil 15571  fclusnei 15607  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomplem 15620  fcluscomp 15621  ufcomp 15622  fclusfnei 15626  filbcmb 15776  heiborlem1 15955  heiborlem28 15982  divrngidl 16176  lubun 16899  lubunNEW 16900  atomnle 17016  grpidNEW 17124

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

Copyright terms: Public domain