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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mp2  16  syl6mpi  64  mp2ani  429  pm2.24i  613  simplimdc  850  mp3an3  1316  3impexpbicom  1426  mpisyl  1434  equcomi  1692  equsex  1716  equsexd  1717  spimt  1724  spimeh  1727  equvini  1746  equveli  1747  sbcof2  1798  dveeq2  1803  ax11v2  1808  ax16i  1846  pm13.183  2864  euxfr2dc  2911  sbcth  2964  sbcth2  3038  ssun3  3287  ssun4  3288  ralf0  3512  exmidexmid  4175  rext  4193  exss  4205  uniopel  4234  onsucelsucexmid  4507  suc11g  4534  eunex  4538  ordsoexmid  4539  tfisi  4564  finds1  4579  omsinds  4599  relop  4754  dmrnssfld  4867  iss  4930  relcoi1  5135  nfunv  5221  funimass2  5266  fvssunirng  5501  fvmptg  5562  oprabidlem  5873  fovcl  5947  elovmpo  6039  tfrlem1  6276  oaword1  6439  0domg  6803  diffifi  6860  exmidpw  6874  djulclb  7020  0ct  7072  nlt1pig  7282  dmaddpq  7320  dmmulpq  7321  archnqq  7358  prarloclemarch2  7360  prarloclemlt  7434  cnegex  8076  nnge1  8880  zneo  9292  fsum2d  11376  fsumabs  11406  fsumiun  11418  fprod2d  11564  efne0  11619  nn0o1gt2  11842  ennnfonelemex  12347  qtopbasss  13171  reeff1o  13344  coseq0negpitopi  13407  cos02pilt1  13422  logltb  13445  bdop  13767  bj-nntrans  13843