Theorem mpi 44

Description: A nested modus ponens inference.

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	. 2 |- ps
2		mpi.2	. . 3 |- (ph -> (ps -> ch))
3	2	com12 13	. 2 |- (ps -> (ph -> ch))
4	1, 3	ax-mp 6	1 |- (ph -> ch)

Syntax hints:   -> wi 2

This theorem is referenced by:  mpii 45  mtoi 94  mt2i 97  mt3i 100  mpbii 168  mpbiri 169  mpan2 519  mpani 521  mp2ani 523  mt2bi 535  tbt 541  ax9 807  eqcom 811  eqvin.l1 851  ceqsex 1370  moeq3 1432  ssun3 1623  ssun4 1624  ssin 1659  difexg 1703  rabexg 1705  prss 1854  tpss 1855  rext 1862  exss 1881  unexb 1950  difex2 1951  uniexb 1962  wefrc 2195  suceloni 2314  ordun 2332  limsssuc 2362  snsn0non 2371  tfinds 2401  dmexg 2551  rnexg 2569  iss 2599  imaexg 2612  cotr 2625  cnvsym 2626  cnvexg 2669  coexg 2671  nfunv 2693  funimass2 2713  resfunexg 2717  fvopab4g 2870  funopfv 2886  canth 2945  oprabval2g 3050  caoprmo 3084  oaordi 3148  oaword2 3155  ecelqsi 3229  mapex 3261  enrefg 3294  xpdom2 3345  sbthlem1 3349  mapdom2 3389  limenpsi 3400  onomeneq 3414  unblem2 3432  suc11reg 3456  inf5 3472  elom3 3478  r1val1 3502  rankwflem 3509  rankr1 3518  rankel 3524  rankpw 3528  r1pwcl 3530  rankun 3535  ranklon 3540  karden 3551  aceq3lem 3555  kmlem2 3581  kmlem9 3588  numthlem 3598  zornlem7 3609  imadomg 3616  carden 3638  carddomi 3641  sdomsdomcard 3654  cardlim 3657  cardiun 3665  axextnd 3737  nlt1pi 3827  indpi 3828  reclem3pr 3952  eqneg 4378  nnge1t 4439  elnnz1 4581  uzind 4603  abslt 4855  absle 4856  infdif 4948  infmap2lem2 4952  hiidge0t 5056  ococint 5298  chsupval2t 5303  chsupvalt 5304  chsupclt 5309  chsupss 5311  shlej1 5349  h1de2 5458  pjss2 5571  pjssm 5572  sto2 5678  stge1 5679  stle0 5680  stle 5681  stles 5682  stm1 5684  stadd 5687  stadd3 5689  strlem6 5697  golem1 5704  stcltrlem1 5709  dmdbr2 5733  hatomistic 5755

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org