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  432  pm2.24i  624  simplimdc  861  mp3an3  1337  3impexpbicom  1449  mpisyl  1457  equcomi  1715  equsex  1739  equsexd  1740  spimt  1747  spimeh  1750  equvini  1769  equveli  1770  sbcof2  1821  dveeq2  1826  ax11v2  1831  ax16i  1869  pm13.183  2894  euxfr2dc  2941  sbcth  2995  sbcth2  3069  ssun3  3320  ssun4  3321  ralf0  3545  exmidexmid  4221  rext  4240  exss  4252  uniopel  4281  onsucelsucexmid  4554  suc11g  4581  eunex  4585  ordsoexmid  4586  tfisi  4611  finds1  4626  omsinds  4646  relop  4802  dmrnssfld  4915  iss  4978  relcoi1  5185  nfunv  5275  funimass2  5320  fvssunirng  5557  fvmptg  5621  oprabidlem  5937  elovmpo  6105  tfrlem1  6348  oaword1  6511  0domg  6880  diffifi  6937  exmidpw  6951  djulclb  7100  0ct  7152  nlt1pig  7387  dmaddpq  7425  dmmulpq  7426  archnqq  7463  prarloclemarch2  7465  prarloclemlt  7539  cnegex  8183  nnge1  8991  zneo  9404  fsum2d  11552  fsumabs  11582  fsumiun  11594  fprod2d  11740  efne0  11795  nn0o1gt2  12020  ennnfonelemex  12545  qtopbasss  14646  ivthdichlem  14762  reeff1o  14836  coseq0negpitopi  14899  cos02pilt1  14914  logltb  14937  gausslemma2dlem0i  15101  bdop  15291  bj-nntrans  15367