Theorem mpan2 422

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpanr12  436  mp3an23  1311  equs4  1705  sb4bor  1815  elvd  2717  eueq2dc  2885  sbcgf  3004  csbconstgf  3044  sbcnestg  3084  csbnestg  3085  csbnest1g  3086  ssindif0im  3453  mpteq1  4048  iinexgm  4115  mss  4185  eusv2nf  4414  eldifpw  4435  ordtriexmid  4478  onsucsssucexmid  4484  ordsucunielexmid  4488  nn0suc  4561  xpss1  4693  xpiindim  4720  reldm0  4801  elrnmpt1s  4833  resdm  4902  resid  4919  eliniseg  4953  trinxp  4976  inimasn  5000  ssrnres  5025  cnveq0  5039  coi2  5099  relrelss  5109  funcnvres  5240  funimaex  5252  fnresin1  5281  fnresin2  5282  fresin  5345  dffv3g  5461  ssimaex  5526  dmfco  5533  fvmpt  5542  fsn  5636  fsn2  5638  elabrex  5703  f1elima  5718  2ndconst  6163  tposfun  6201  tpostpos2  6206  tfrexlem  6275  tfri3  6308  rdgruledefgg  6316  rdgss  6324  frecsuclem  6347  frecrdg  6349  oa0  6397  om0  6398  oei0  6399  oav2  6403  oa1suc  6407  nnmsucr  6428  nnm1  6464  nnm2  6465  ecelqsg  6526  ecidg  6537  xpider  6544  qsel  6550  mapdm0  6601  map0e  6624  mapsnconst  6632  ixpsnf1o  6674  map1  6750  xp1en  6761  xpcomco  6764  xpmapenlem  6787  findcard2s  6828  findcard2d  6829  findcard2sd  6830  exmidpw  6846  fidcenumlemr  6892  sbthlem7  6900  eqinfti  6956  djueq1  6974  omp1eomlem  7028  endjusym  7030  eninl  7031  eninr  7032  difinfsn  7034  finomni  7066  pm54.43  7108  exmidonfinlem  7111  mulidpi  7221  nlt1pig  7244  indpi  7245  halfnqq  7313  archnqq  7320  prarloclemarch  7321  prarloclemarch2  7322  nnnq  7325  nq0a0  7360  addpinq1  7367  prarloclemlt  7396  prarloclemlo  7397  prarloclem3  7400  prarloclemcalc  7405  nqprm  7445  addnqpr1  7465  1idprl  7493  1idpru  7494  1idpr  7495  recexprlem1ssl  7536  recexprlem1ssu  7537  ltmprr  7545  0idsr  7670  1idsr  7671  00sr  7672  pn0sr  7674  negexsr  7675  recexgt0sr  7676  ltm1sr  7680  archsr  7685  prsrcl  7687  prsradd  7689  mappsrprg  7707  map2psrprg  7708  elrealeu  7732  pitonnlem1p1  7749  peano2nnnn  7756  ax1rid  7780  axcnre  7784  peano5nnnn  7795  peano2cn  7993  peano2re  7994  addid2  7997  subid  8077  subid1  8078  negid  8105  negeq0  8112  peano2cnm  8124  peano2rem  8125  mul01  8247  lt0neg1  8326  le0neg1  8328  recexre  8436  inelr  8442  rimul  8443  reapmul1  8453  apsqgt0  8459  mulge0  8477  negap0  8488  divvalap  8530  rerecclap  8586  div2negap  8591  divgt0i2i  8771  peano5nni  8819  nnge1  8839  times2  8945  addltmul  9052  nn0p1nn  9112  peano2nn0  9113  nn0lele2xi  9124  znnnlt1  9198  nn0lt10b  9227  prime  9246  msqznn  9247  zeo  9252  elnn1uz2  9500  qreccl  9533  qdivcl  9534  irrmul  9538  rphalfcl  9570  rpnegap  9575  zgt1rpn0n1  9584  ltpnf  9669  nltmnf  9677  pnfge  9678  xlt0neg1  9724  xle0neg1  9726  xaddpnf1  9732  xaddmnf1  9734  xaddid1  9748  xsubge0  9767  xleaddadd  9773  elioopnf  9853  elicopnf  9855  iccshftri  9881  iccshftli  9883  iccdili  9885  icccntri  9887  fzprval  9966  fzofzp1  10108  fzostep1  10118  flqge0nn0  10174  flqge1nn  10175  fldiv4p1lem1div2  10186  exp1  10407  qexpclz  10422  nn0sqcl  10428  expeq0  10432  expubnd  10458  sqval  10459  sqeq0  10464  resqcl  10468  zsqcl  10471  iexpcyc  10505  binom21  10512  bcnn  10613  bcn2  10620  bcn2p1  10626  bcnm1  10628  fihasheq0  10650  hashsng  10654  fihashen1  10655  fimaxq  10683  shftfibg  10702  shftfib  10705  reim0  10743  imval2  10776  cjap0  10789  cjne0  10790  rexuz3  10872  resqrexlemover  10892  abssq  10963  nn0abscl  10967  nnabscl  10982  abs2dif  10988  max0addsup  11101  climshft  11183  bcxmas  11368  efgt1p2  11574  efgt1p  11575  efi4p  11596  resin4p  11597  recos4p  11598  sinbnd  11631  cosbnd  11632  dvdsval2  11668  zdvdsdc  11689  dvdsmul2  11691  dvdsmulcr  11698  dvdsabseq  11720  divconjdvds  11722  alzdvds  11727  fzo0dvdseq  11730  odd2np1lem  11744  mod2eq1n2dvds  11751  flodddiv4  11806  flodddiv4t2lthalf  11809  gcdmndc  11812  gcd0id  11843  gcd1  11851  dfgcd2  11878  gcdmultiple  11884  gcdmultiplez  11885  dvdssq  11895  lcmmndc  11919  lcm0val  11922  dvdslcm  11926  lcmeq0  11928  lcmgcd  11935  lcmdvds  11936  lcmid  11937  lcm1  11938  cncongr2  11961  isprm3  11975  prm2orodd  11983  sqrt2irrap  12034  phiprm  12075  unennn  12098  ennnfonelemim  12125  ctinfom  12129  ctinf  12131  enctlem  12133  ressid  12211  elrestr  12319  0opn  12364  topopn  12366  tgval  12409  tgvalex  12410  0cld  12472  ntropn  12477  ntrtop  12488  ntr0  12494  neipsm  12514  rest0  12539  xmetres  12742  metres  12743  mopnex  12865  tgioo  12906  cnlimcim  13000  cnlimc  13001  dvfre  13034  dveflem  13047  dvef  13048  efcn  13049  sin2pim  13094  cos2pim  13095  sinmpi  13096  cosmpi  13097  sinppi  13098  cosppi  13099  efimpi  13100  sincosq1lem  13106  sincosq2sgn  13108  sincosq3sgn  13109  sincosq4sgn  13110  sinq12gt0  13111  sinq34lt0t  13112  sincosq1eq  13120  abssinper  13127  logrpap0b  13157  loglt1b  13174  rpcxp0  13179  rpcxp1  13180  rpcxpsqrt  13202  logsqrt  13203  rprelogbdiv  13234  bj-inf2vnlem1  13505  pwle2  13531  pwf1oexmid  13532  exmid1stab  13533  nninfsellemeqinf  13551  sbthom  13560  iswomninnlem  13583  redc0  13591