Theorem mpan2 403

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	⊢ ψ
mpan2.2	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
mpan2	⊢ (φ → χ)

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 ⊢ ψ
2	1	a1i 9	. 2 ⊢ (φ → ψ)
3		mpan2.2	. 2 ⊢ ((φ ∧ ψ) → χ)
4	2, 3	mpdan 400	1 ⊢ (φ → χ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  mpanr12  418  mp3an23  1209  equs4  1595  sb4bor  1698  eueq2dc  2691  sbcgf  2802  csbconstgf  2840  sbcnestg  2876  csbnestg  2877  csbnest1g  2878  ssindif0im  3258  mpteq1  3815  iinexgm  3882  mss  3936  eusv2nf  4138  eldifpw  4158  ordtriexmid  4194  onsucsssucexmid  4196  ordsucunielexmid  4200  nn0suc  4254  xpss1  4375  xpiindim  4400  reldm0  4480  elrnmpt1s  4511  resdm  4576  resid  4589  eliniseg  4622  trinxp  4645  inimasn  4668  ssrnres  4690  cnveq0  4704  coi2  4764  relrelss  4771  funcnvres  4898  funimaex  4910  fnresin1  4939  fnresin2  4940  fresin  4993  dffv3g  5099  ssimaex  5159  dmfco  5166  fvmpt  5174  fsn  5260  fsn2  5262  elabrex  5322  f1elima  5337  2ndconst  5766  tposfun  5797  tpostpos2  5802  tfrexlem  5870  tfri3  5875  rdgruledefgg  5882  rdgi0g  5886  rdgss  5890  frec0g  5902  frecsuclem3  5906  oa0  5952  om0  5953  oei0  5954  oav2  5958  oa1suc  5962  nnmsucr  5982  nnm1  6008  nnm2  6009  ecelqsg  6070  ecidg  6081  xpiderm  6088  qsel  6094  mulidpi  6178  nlt1pig  6201  halfnqq  6267  archnqq  6274  prarloclemarch  6275  prarloclemarch2  6276  nq0a0  6312  prarloclemlt  6347  prarloclemlo  6348  prarloclem3  6351  prarloclemcalc  6356  nqprm  6397  1idprl  6429  1idpru  6430  1idpr  6431  recexprlem1ssl  6467  recexprlem1ssu  6468  0idsr  6514  1idsr  6515  00sr  6516  pn0sr  6518  negexsr  6519  recexsrlem  6520  ax1rid  6571  axcnre  6575  peano2cn  6735  peano2re  6736  addid2  6739  subid  6816  subid1  6817  negid  6844  negeq0  6851  peano2cnm  6863  peano2rem  6864  mul01  6972  bj-inf2vnlem1  7188