Theorem mpi 44

Description: A nested modus ponens inference. (The proof was shortened by Stefan Allan, 20-Mar-2006.

Hypotheses

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

Assertion

Ref	Expression
mpi	|- (ph -> ch)

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 |- ps
2	1	a1i 8	. 2 |- (ph -> ps)
3		mpi.2	. 2 |- (ph -> (ps -> ch))
4	2, 3	mpd 26	1 |- (ph -> ch)

Syntax hints:   -> wi 3

This theorem is referenced by:  mpii 45  mtoi 107  mt2i 110  mt3i 113  mpbii 193  mpbiri 194  mpan2 695  mpani 697  mp2ani 699  mt2bi 712  ax4 970  ax9o 1120  equcomi 1126  equvini 1166  ax11v2 1213  ax16i 1268  ax11eq 1361  ax11el 1362  ax11inda 1369  a12stdy1 1370  a12study 1376  ceqsex 1830  moeq3 1917  sbcth 1942  ssun3 2191  ssun4 2192  ssin 2228  ralf0 2355  prss 2467  tpss 2472  dtruALT 2743  rext 2749  exss 2764  uniopel 2804  wefrc 2938  suceloni 3057  ordun 3076  limsssuc 3116  snsn0non 3120  finds1 3154  relop 3270  dmrnssfld 3351  iss 3389  cotr 3428  cnvsym 3429  coexg 3516  nfunv 3538  funimass2 3565  fvopab4g 3770  funfvop 3794  canth 3898  foprcl 4006  oprabval2gf 4017  oaordi 4170  oaword2 4177  oeworde 4210  oelim2 4212  ecelqsi 4282  enrefg 4377  xpdom2 4428  sbthlem1 4433  mapdom2 4480  limenpsi 4491  onomeneq 4504  suc11reg 4585  infeq5 4601  elom3 4611  r1val1 4638  rankwflem 4645  rankr1 4654  rankel 4660  rankpw 4664  r1pwcl 4667  rankun 4671  rankval4 4682  karden 4706  kmlem2 4746  kmlem10 4754  zorn2lem7 4774  imadomg 4786  unidom 4788  carden 4811  cardsn 4814  carddomi 4815  sdomsdomcard 4828  cardlim 4831  cardiun 4839  alephfplem3 4878  alephval2 4882  axextnd 4923  nlt1pi 5013  indpi 5014  reclem3pr 5138  cnegext 5328  eqneg 5768  nnge1t 5899  elnnz1 6110  uzindOLD 6164  inelr 6673  abslt 6818  absle 6819  absltOLD 6820  absleOLD 6821  cvgratlem1ALT 7190  ivthlem3 7226  infcda 7518  infdif 7519  infxp 7523  infmap2lem2 7530  ghgrpilem1 8085  spwval2 8595  logltbt 8715  axgroth3 8718  grothinf 8720  hiidge0t 8903  ococint 9235  chsupval2t 9240  chsupvalt 9241  chsupclt 9246  chsupss 9248  shlej1 9286  h1de2 9414  pjss2 9565  pjssm 9566  sto2 10102  stge1 10103  stle0 10104  stle 10105  stles 10106  stm1 10108  stadd 10111  stadd3 10113  strlem6 10121  golem1 10136  stcltrlem1 10141  mdexch 10199  hatomistic 10226  irredt 10259  atabs 10265  filintf 10479  cnfilca 10487  dtt2 10498

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

Copyright terms: Public domain