Theorem mpi 15

Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Hypotheses

Ref	Expression
mpi.1	⊢ 𝜓
mpi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpi	⊢ (𝜑 → 𝜒)

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4

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

This theorem is referenced by:  mp2  16  syl6mpi  64  mp2ani  424  pm2.24i  589  simplimdc  796  mp3an3  1263  3impexpbicom  1373  mpisyl  1381  equcomi  1638  equsex  1664  equsexd  1665  spimt  1672  spimeh  1675  equvini  1689  equveli  1690  sbcof2  1739  dveeq2  1744  ax11v2  1749  ax16i  1787  pm13.183  2755  euxfr2dc  2801  sbcth  2854  sbcth2  2927  ssun3  3166  ssun4  3167  ralf0  3389  exmidexmid  4037  rext  4051  exss  4063  uniopel  4092  onsucelsucexmid  4359  suc11g  4386  eunex  4390  ordsoexmid  4391  tfisi  4415  finds1  4430  omsinds  4448  relop  4599  dmrnssfld  4709  iss  4771  relcoi1  4975  nfunv  5060  funimass2  5105  fvssunirng  5333  fvmptg  5393  oprabidlem  5694  fovcl  5764  elovmpt2  5859  tfrlem1  6087  oaword1  6246  0domg  6607  diffifi  6664  exmidpw  6678  djulclb  6801  nlt1pig  6954  dmaddpq  6992  dmmulpq  6993  archnqq  7030  prarloclemarch2  7032  prarloclemlt  7106  cnegex  7714  nnge1  8499  zneo  8901  fsum2d  10883  fsumabs  10913  fsumiun  10925  efne0  11022  nn0o1gt2  11237  bdop  12032  bj-nntrans  12112