Theorem mpan2 421

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 417	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  435  mp3an23  1307  equs4  1703  sb4bor  1807  elvd  2691  eueq2dc  2857  sbcgf  2976  csbconstgf  3015  sbcnestg  3053  csbnestg  3054  csbnest1g  3055  ssindif0im  3422  mpteq1  4012  iinexgm  4079  mss  4148  eusv2nf  4377  eldifpw  4398  ordtriexmid  4437  onsucsssucexmid  4442  ordsucunielexmid  4446  nn0suc  4518  xpss1  4649  xpiindim  4676  reldm0  4757  elrnmpt1s  4789  resdm  4858  resid  4875  eliniseg  4909  trinxp  4932  inimasn  4956  ssrnres  4981  cnveq0  4995  coi2  5055  relrelss  5065  funcnvres  5196  funimaex  5208  fnresin1  5237  fnresin2  5238  fresin  5301  dffv3g  5417  ssimaex  5482  dmfco  5489  fvmpt  5498  fsn  5592  fsn2  5594  elabrex  5659  f1elima  5674  2ndconst  6119  tposfun  6157  tpostpos2  6162  tfrexlem  6231  tfri3  6264  rdgruledefgg  6272  rdgss  6280  frecsuclem  6303  frecrdg  6305  oa0  6353  om0  6354  oei0  6355  oav2  6359  oa1suc  6363  nnmsucr  6384  nnm1  6420  nnm2  6421  ecelqsg  6482  ecidg  6493  xpider  6500  qsel  6506  mapdm0  6557  map0e  6580  mapsnconst  6588  ixpsnf1o  6630  map1  6706  xp1en  6717  xpcomco  6720  xpmapenlem  6743  findcard2s  6784  findcard2d  6785  findcard2sd  6786  exmidpw  6802  fidcenumlemr  6843  sbthlem7  6851  eqinfti  6907  djueq1  6925  omp1eomlem  6979  endjusym  6981  eninl  6982  eninr  6983  difinfsn  6985  finomni  7012  pm54.43  7046  exmidonfinlem  7049  mulidpi  7126  nlt1pig  7149  indpi  7150  halfnqq  7218  archnqq  7225  prarloclemarch  7226  prarloclemarch2  7227  nnnq  7230  nq0a0  7265  addpinq1  7272  prarloclemlt  7301  prarloclemlo  7302  prarloclem3  7305  prarloclemcalc  7310  nqprm  7350  addnqpr1  7370  1idprl  7398  1idpru  7399  1idpr  7400  recexprlem1ssl  7441  recexprlem1ssu  7442  ltmprr  7450  0idsr  7575  1idsr  7576  00sr  7577  pn0sr  7579  negexsr  7580  recexgt0sr  7581  ltm1sr  7585  archsr  7590  prsrcl  7592  prsradd  7594  mappsrprg  7612  map2psrprg  7613  elrealeu  7637  pitonnlem1p1  7654  peano2nnnn  7661  ax1rid  7685  axcnre  7689  peano5nnnn  7700  peano2cn  7897  peano2re  7898  addid2  7901  subid  7981  subid1  7982  negid  8009  negeq0  8016  peano2cnm  8028  peano2rem  8029  mul01  8151  lt0neg1  8230  le0neg1  8232  recexre  8340  inelr  8346  rimul  8347  reapmul1  8357  apsqgt0  8363  mulge0  8381  negap0  8392  divvalap  8434  rerecclap  8490  div2negap  8495  divgt0i2i  8675  peano5nni  8723  nnge1  8743  times2  8849  addltmul  8956  nn0p1nn  9016  peano2nn0  9017  nn0lele2xi  9028  znnnlt1  9102  nn0lt10b  9131  prime  9150  msqznn  9151  zeo  9156  elnn1uz2  9401  qreccl  9434  qdivcl  9435  irrmul  9439  rphalfcl  9469  rpnegap  9474  ltpnf  9567  nltmnf  9574  pnfge  9575  xlt0neg1  9621  xle0neg1  9623  xaddpnf1  9629  xaddmnf1  9631  xaddid1  9645  xsubge0  9664  xleaddadd  9670  elioopnf  9750  elicopnf  9752  iccshftri  9778  iccshftli  9780  iccdili  9782  icccntri  9784  fzprval  9862  fzofzp1  10004  fzostep1  10014  flqge0nn0  10066  flqge1nn  10067  fldiv4p1lem1div2  10078  exp1  10299  qexpclz  10314  nn0sqcl  10320  expeq0  10324  expubnd  10350  sqval  10351  sqeq0  10356  resqcl  10360  zsqcl  10363  iexpcyc  10397  binom21  10404  bcnn  10503  bcn2  10510  bcn2p1  10516  bcnm1  10518  fihasheq0  10540  hashsng  10544  fihashen1  10545  fimaxq  10573  shftfibg  10592  shftfib  10595  reim0  10633  imval2  10666  cjap0  10679  cjne0  10680  rexuz3  10762  resqrexlemover  10782  abssq  10853  nn0abscl  10857  nnabscl  10872  abs2dif  10878  max0addsup  10991  climshft  11073  bcxmas  11258  efgt1p2  11401  efgt1p  11402  efi4p  11424  resin4p  11425  recos4p  11426  sinbnd  11459  cosbnd  11460  dvdsval2  11496  zdvdsdc  11514  dvdsmul2  11516  dvdsmulcr  11523  dvdsabseq  11545  divconjdvds  11547  alzdvds  11552  fzo0dvdseq  11555  odd2np1lem  11569  mod2eq1n2dvds  11576  flodddiv4  11631  flodddiv4t2lthalf  11634  gcdmndc  11637  gcd0id  11667  gcd1  11675  dfgcd2  11702  gcdmultiple  11708  gcdmultiplez  11709  dvdssq  11719  lcmmndc  11743  lcm0val  11746  dvdslcm  11750  lcmeq0  11752  lcmgcd  11759  lcmdvds  11760  lcmid  11761  lcm1  11762  cncongr2  11785  isprm3  11799  prm2orodd  11807  sqrt2irrap  11858  phiprm  11899  unennn  11910  ennnfonelemim  11937  ctinfom  11941  ctinf  11943  enctlem  11945  ressid  12020  elrestr  12128  0opn  12173  topopn  12175  tgval  12218  tgvalex  12219  0cld  12281  ntropn  12286  ntrtop  12297  ntr0  12303  neipsm  12323  rest0  12348  xmetres  12551  metres  12552  mopnex  12674  tgioo  12715  cnlimcim  12809  cnlimc  12810  dvfre  12843  dveflem  12855  dvef  12856  efcn  12857  sin2pim  12894  cos2pim  12895  sinmpi  12896  cosmpi  12897  sinppi  12898  cosppi  12899  efimpi  12900  sincosq1lem  12906  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  sinq34lt0t  12912  sincosq1eq  12920  abssinper  12927  bj-inf2vnlem1  13168  pwle2  13193  pwf1oexmid  13194  exmid1stab  13195  nninfsellemeqinf  13212  sbthom  13221