Theorem mpi 55

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 29	1 |- (ph -> ch)

Syntax hints:   -> wi 3

This theorem is referenced by:  mpii 56  mtoi 122  mt2i 125  mt3i 128  mpbii 210  mpbiri 211  mpan2 760  mpani 762  mp2ani 764  mt2bi 781  3impexp 1286  3impexpbicom 1287  ax4 1318  ax9o 1480  equcomi 1487  equviniOLD 1532  ax11v2 1585  ax16i 1647  ax11eq 1754  ax11el 1755  ax11inda 1762  a12stdy1 1763  a12study 1769  ceqsex 2324  moeq3 2432  sbcth 2458  ssun3 2769  ssun4 2770  ssinOLD 2815  ralf0 2975  prssOLD 3139  tpssOLD 3146  uniintsn 3253  elOLD 3486  dtru 3498  rext 3502  exss 3516  uniopel 3556  wefrc 3652  ordun 3771  snsn0nonOLD 3789  euexeqOLD 3826  euexaleq 3827  limsssuc 3934  finds1 3982  relop 4113  dmrnssfld 4205  iss 4254  issOLD 4255  cotrOLD 4303  cnvsymOLD 4305  coexg 4429  nfunv 4453  funimass2 4492  fvopab4g 4742  fvpr1 4759  fvpr2 4760  fvtp1 4761  fvtp2 4762  fvtp3 4763  funfvop 4776  foprcl 4944  oprabval2gf 4955  canth 5112  oaordi 5227  oaword2 5235  oeworde 5268  oelim2 5270  enrefg 5449  xpdom2 5501  ac6sfilem3 5508  sbthlem1 5510  mapdom2 5588  limenpsi 5599  onomeneq 5612  hartog 5693  suc11reg 5710  infeq5 5727  elom3 5738  r1val1 5769  rankwflem 5776  rankr1 5785  rankel 5791  rankpw 5795  r1pwcl 5798  rankun 5802  rankval4 5813  karden 5856  kmlem2 5928  kmlem10 5936  zorn2lem7 5956  imadomg 5968  unidom 5970  carden 5981  cardsn 5984  carddomi 5986  sdomsdomcard 6000  cardlim 6003  cardiun 6011  alephfplem3 6046  alephval2 6050  nnacda 6088  axextnd 6095  nlt1pi 6185  indpi 6186  reclem3pr 6310  cnegex 6502  eqnegi 6982  nnge1 7126  elnnz1 7364  uzindOLD 7420  zindd 7427  inelr 7985  abslti 8127  abslei 8128  cvgratlem1ALT 8509  ivthlem3 8545  infcda 8836  infdif 8837  infxp 8841  infmap2lem2 8849  ghgrpilem1 9441  spwval2 9996  logltb 10130  grothomex 10136  axgroth3 10138  twpar2 10149  oprabco 10159  findcardOLD 10179  filintf 10274  usinuniop 10341  dvrunz 10419  hiidge0 10597  ococin 10930  chsupval2 10935  chsupval 10936  chsupcl 10941  chsupss 10943  shlej1i 10981  h1de2i 11109  pjss2i 11260  pjssmii 11261  sto2i 11809  stge1i 11810  stle0i 11811  stlei 11812  stlesi 11813  stm1i 11815  staddi 11818  stadd3i 11820  strlem6 11828  golem1 11843  stcltrlem1 11848  mdexchi 11907  hatomistici 11934  irred 11967  atabsi 11973  bnj1430 13125  bnj97 13220  bnj966 13348  ifexg 13599  dvdslelem 13692  gcdaddmlem 13734  zgt1b1 13771  frxp 13951  wfrlem5 13961  wfrlem16 13972  tfrALTlem 13976  nofv 13998  noprc 14018  axfelem10 14040  axfelem15 14045  merco2 14203  evpexun 14322  uuniin 14405  cmprelid2 14447  islatalg 14531  tolat 14631  fincmpzer 14711  fprodsub 14742  top2usne 14898  cnfilca 14927  rcfpfil 14934  limvinlv 14941  dtt2 14951  bwt2 14960  cntrsetlem 14999  dualalg 15131  emptar 15231  intartar 15255  hartogOLD 15384  alexsublem2 15438  alexsublem4 15440  ufileulem 15572  prfv1OLD 15678  prfv2OLD 15679  abrexdom 15739  findcard2 15745  fimax 15746  fimaxre 15774  heiborlem13 15967  heiborlem16 15970  heiborlem41 15995  bfplem5 16002  bfplem8 16005  bfplem9 16006  pcopt 16084  ax4567to4 16360  pm13.183 16373  pltirr 16784  pmodi 17309  osumcllem11 17374  pexmidlem8 17385

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

Copyright terms: Public domain