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  623  simplimdc  860  mp3an3  1326  3impexpbicom  1438  mpisyl  1446  equcomi  1704  equsex  1728  equsexd  1729  spimt  1736  spimeh  1739  equvini  1758  equveli  1759  sbcof2  1810  dveeq2  1815  ax11v2  1820  ax16i  1858  pm13.183  2875  euxfr2dc  2922  sbcth  2976  sbcth2  3050  ssun3  3300  ssun4  3301  ralf0  3526  exmidexmid  4194  rext  4213  exss  4225  uniopel  4254  onsucelsucexmid  4527  suc11g  4554  eunex  4558  ordsoexmid  4559  tfisi  4584  finds1  4599  omsinds  4619  relop  4774  dmrnssfld  4887  iss  4950  relcoi1  5157  nfunv  5246  funimass2  5291  fvssunirng  5527  fvmptg  5589  oprabidlem  5901  fovcl  5975  elovmpo  6067  tfrlem1  6304  oaword1  6467  0domg  6832  diffifi  6889  exmidpw  6903  djulclb  7049  0ct  7101  nlt1pig  7335  dmaddpq  7373  dmmulpq  7374  archnqq  7411  prarloclemarch2  7413  prarloclemlt  7487  cnegex  8129  nnge1  8936  zneo  9348  fsum2d  11434  fsumabs  11464  fsumiun  11476  fprod2d  11622  efne0  11677  nn0o1gt2  11900  ennnfonelemex  12405  qtopbasss  13803  reeff1o  13976  coseq0negpitopi  14039  cos02pilt1  14054  logltb  14077  bdop  14398  bj-nntrans  14474