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  4196  rext  4215  exss  4227  uniopel  4256  onsucelsucexmid  4529  suc11g  4556  eunex  4560  ordsoexmid  4561  tfisi  4586  finds1  4601  omsinds  4621  relop  4777  dmrnssfld  4890  iss  4953  relcoi1  5160  nfunv  5249  funimass2  5294  fvssunirng  5530  fvmptg  5592  oprabidlem  5905  fovcl  5979  elovmpo  6071  tfrlem1  6308  oaword1  6471  0domg  6836  diffifi  6893  exmidpw  6907  djulclb  7053  0ct  7105  nlt1pig  7339  dmaddpq  7377  dmmulpq  7378  archnqq  7415  prarloclemarch2  7417  prarloclemlt  7491  cnegex  8134  nnge1  8941  zneo  9353  fsum2d  11442  fsumabs  11472  fsumiun  11484  fprod2d  11630  efne0  11685  nn0o1gt2  11909  ennnfonelemex  12414  qtopbasss  13991  reeff1o  14164  coseq0negpitopi  14227  cos02pilt1  14242  logltb  14265  bdop  14597  bj-nntrans  14673