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  846  mp3an3  1308  3impexpbicom  1418  mpisyl  1426  equcomi  1684  equsex  1708  equsexd  1709  spimt  1716  spimeh  1719  equvini  1738  equveli  1739  sbcof2  1790  dveeq2  1795  ax11v2  1800  ax16i  1838  pm13.183  2850  euxfr2dc  2897  sbcth  2950  sbcth2  3024  ssun3  3272  ssun4  3273  ralf0  3497  exmidexmid  4157  rext  4175  exss  4187  uniopel  4216  onsucelsucexmid  4488  suc11g  4515  eunex  4519  ordsoexmid  4520  tfisi  4545  finds1  4560  omsinds  4580  relop  4735  dmrnssfld  4848  iss  4911  relcoi1  5116  nfunv  5202  funimass2  5247  fvssunirng  5482  fvmptg  5543  oprabidlem  5849  fovcl  5923  elovmpo  6018  tfrlem1  6252  oaword1  6415  0domg  6779  diffifi  6836  exmidpw  6850  djulclb  6993  0ct  7045  nlt1pig  7255  dmaddpq  7293  dmmulpq  7294  archnqq  7331  prarloclemarch2  7333  prarloclemlt  7407  cnegex  8047  nnge1  8850  zneo  9259  fsum2d  11325  fsumabs  11355  fsumiun  11367  fprod2d  11513  efne0  11568  nn0o1gt2  11788  ennnfonelemex  12126  qtopbasss  12892  reeff1o  13065  coseq0negpitopi  13128  cos02pilt1  13143  logltb  13166  bdop  13421  bj-nntrans  13497