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  430  pm2.24i  618  simplimdc  855  mp3an3  1321  3impexpbicom  1431  mpisyl  1439  equcomi  1697  equsex  1721  equsexd  1722  spimt  1729  spimeh  1732  equvini  1751  equveli  1752  sbcof2  1803  dveeq2  1808  ax11v2  1813  ax16i  1851  pm13.183  2868  euxfr2dc  2915  sbcth  2968  sbcth2  3042  ssun3  3292  ssun4  3293  ralf0  3518  exmidexmid  4182  rext  4200  exss  4212  uniopel  4241  onsucelsucexmid  4514  suc11g  4541  eunex  4545  ordsoexmid  4546  tfisi  4571  finds1  4586  omsinds  4606  relop  4761  dmrnssfld  4874  iss  4937  relcoi1  5142  nfunv  5231  funimass2  5276  fvssunirng  5511  fvmptg  5572  oprabidlem  5884  fovcl  5958  elovmpo  6050  tfrlem1  6287  oaword1  6450  0domg  6815  diffifi  6872  exmidpw  6886  djulclb  7032  0ct  7084  nlt1pig  7303  dmaddpq  7341  dmmulpq  7342  archnqq  7379  prarloclemarch2  7381  prarloclemlt  7455  cnegex  8097  nnge1  8901  zneo  9313  fsum2d  11398  fsumabs  11428  fsumiun  11440  fprod2d  11586  efne0  11641  nn0o1gt2  11864  ennnfonelemex  12369  qtopbasss  13315  reeff1o  13488  coseq0negpitopi  13551  cos02pilt1  13566  logltb  13589  bdop  13910  bj-nntrans  13986