Theorem mpan2 416

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 412	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpanr12  430  mp3an23  1263  equs4  1657  sb4bor  1760  eueq2dc  2779  sbcgf  2895  csbconstgf  2933  sbcnestg  2970  csbnestg  2971  csbnest1g  2972  ssindif0im  3330  mpteq1  3897  iinexgm  3964  mss  4026  eusv2nf  4251  eldifpw  4271  ordtriexmid  4310  onsucsssucexmid  4315  ordsucunielexmid  4319  nn0suc  4391  xpss1  4515  xpiindim  4540  reldm0  4621  elrnmpt1s  4652  resdm  4717  resid  4732  eliniseg  4766  trinxp  4789  inimasn  4812  ssrnres  4836  cnveq0  4850  coi2  4910  relrelss  4920  funcnvres  5049  funimaex  5061  fnresin1  5090  fnresin2  5091  fresin  5146  dffv3g  5258  ssimaex  5322  dmfco  5329  fvmpt  5338  fsn  5426  fsn2  5428  elabrex  5492  f1elima  5507  2ndconst  5938  tposfun  5973  tpostpos2  5978  tfrexlem  6047  tfri3  6080  rdgruledefgg  6088  rdgss  6096  frecsuclem  6119  frecrdg  6121  oa0  6166  om0  6167  oei0  6168  oav2  6172  oa1suc  6176  nnmsucr  6197  nnm1  6229  nnm2  6230  ecelqsg  6291  ecidg  6302  xpiderm  6309  qsel  6315  mapdm0  6366  map0e  6389  mapsnconst  6397  map1  6475  xp1en  6485  xpcomco  6488  xpmapenlem  6511  findcard2s  6552  findcard2d  6553  findcard2sd  6554  exmidpw  6570  sbthlem7  6609  eqinfti  6652  djueq1  6670  finomni  6733  pm54.43  6755  mulidpi  6814  nlt1pig  6837  indpi  6838  halfnqq  6906  archnqq  6913  prarloclemarch  6914  prarloclemarch2  6915  nnnq  6918  nq0a0  6953  addpinq1  6960  prarloclemlt  6989  prarloclemlo  6990  prarloclem3  6993  prarloclemcalc  6998  nqprm  7038  addnqpr1  7058  1idprl  7086  1idpru  7087  1idpr  7088  recexprlem1ssl  7129  recexprlem1ssu  7130  ltmprr  7138  0idsr  7250  1idsr  7251  00sr  7252  pn0sr  7254  negexsr  7255  recexgt0sr  7256  archsr  7264  prsrcl  7266  prsradd  7268  elrealeu  7304  pitonnlem1p1  7320  peano2nnnn  7327  ax1rid  7349  axcnre  7353  peano5nnnn  7364  peano2cn  7554  peano2re  7555  addid2  7558  subid  7638  subid1  7639  negid  7666  negeq0  7673  peano2cnm  7685  peano2rem  7686  mul01  7804  lt0neg1  7883  le0neg1  7885  recexre  7989  inelr  7995  rimul  7996  reapmul1  8006  apsqgt0  8012  mulge0  8030  negap0  8040  divvalap  8073  rerecclap  8129  div2negap  8134  divgt0i2i  8306  peano5nni  8353  nnge1  8373  times2  8472  addltmul  8578  nn0p1nn  8638  peano2nn0  8639  nn0lele2xi  8650  znnnlt1  8724  nn0lt10b  8753  prime  8771  msqznn  8772  zeo  8777  elnn1uz2  9019  qreccl  9052  qdivcl  9053  irrmul  9057  rphalfcl  9086  rpnegap  9091  ltpnf  9176  nltmnf  9183  pnfge  9184  xlt0neg1  9225  xle0neg1  9227  elioopnf  9310  elicopnf  9312  iccshftri  9337  iccshftli  9339  iccdili  9341  icccntri  9343  fzprval  9419  fzofzp1  9559  fzostep1  9569  flqge0nn0  9621  flqge1nn  9622  fldiv4p1lem1div2  9633  expivallem  9847  expival  9848  exp1  9852  qexpclz  9867  nn0sqcl  9873  expeq0  9877  expubnd  9903  sqval  9904  sqeq0  9909  resqcl  9913  zsqcl  9916  iexpcyc  9949  binom21  9956  bcnn  10054  bcn2  10061  bcn2p1  10067  bcnm1  10069  fihasheq0  10091  hashsng  10095  fihashen1  10096  fimaxq  10124  shftfibg  10143  shftfib  10146  reim0  10183  imval2  10216  cjap0  10229  cjne0  10230  rexuz3  10311  resqrexlemover  10331  abs00  10385  abssq  10402  nn0abscl  10406  nnabscl  10421  abs2dif  10427  max0addsup  10540  climshft  10578  dvdsval2  10666  zdvdsdc  10684  dvdsmul2  10686  dvdsmulcr  10693  dvdsabseq  10715  divconjdvds  10717  alzdvds  10722  fzo0dvdseq  10725  odd2np1lem  10739  mod2eq1n2dvds  10746  flodddiv4  10801  flodddiv4t2lthalf  10804  gcdmndc  10807  gcd0id  10837  gcd1  10845  dfgcd2  10870  gcdmultiple  10876  gcdmultiplez  10877  dvdssq  10887  lcmmndc  10911  lcm0val  10914  dvdslcm  10918  lcmeq0  10920  lcmgcd  10927  lcmdvds  10928  lcmid  10929  lcm1  10930  cncongr2  10953  isprm3  10967  prm2orodd  10975  sqrt2irrap  11025  phiprm  11066  unennn  11077  bj-inf2vnlem1  11295  nninfsellemeqinf  11338