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  628  simplimdc  868  mp3an3  1363  3impexpbicom  1484  mpisyl  1492  equcomi  1752  equsex  1776  equsexd  1778  spimt  1785  spimeh  1788  equvini  1807  equveli  1808  sbcof2  1859  dveeq2  1864  ax11v2  1869  ax16i  1907  pm13.183  2955  euxfr2dc  3002  sbcth  3056  sbcth2  3131  ssun3  3384  ssun4  3385  ralf0  3612  exmidexmid  4309  rext  4331  exss  4343  uniopel  4373  onsucelsucexmid  4652  suc11g  4679  eunex  4683  ordsoexmid  4684  tfisi  4709  finds1  4724  omsinds  4744  relop  4905  dmrnssfld  5020  iss  5084  relcoi1  5294  nfunv  5385  funimass2  5434  fvssunirng  5685  fvmptg  5753  oprabidlem  6081  elovmpo  6253  tfrlem1  6539  oaword1  6704  modom  7061  0domg  7090  1ndom2  7119  diffifi  7151  exmidpw  7168  djulclb  7346  0ct  7398  iftrueb01  7533  nlt1pig  7656  dmaddpq  7694  dmmulpq  7695  archnqq  7732  prarloclemarch2  7734  prarloclemlt  7808  cnegex  8451  nnge1  9260  zneo  9679  fsum2d  12121  fsumabs  12151  fsumiun  12163  fprod2d  12309  efne0  12364  nn0o1gt2  12591  ennnfonelemex  13165  qtopbasss  15386  ivthdichlem  15516  dvmptfsum  15590  reeff1o  15638  coseq0negpitopi  15701  cos02pilt1  15716  logltb  15739  pellexlem3  15847  gausslemma2dlem0i  15930  2lgs  15977  bdop  16645  bj-nntrans  16721  exmidcon  16780