Theorem mpan2 425

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mpanr12  439  mp3an23  1363  equs4  1771  sb4bor  1881  elvd  2804  eueq2dc  2976  sbcgf  3096  csbconstgf  3137  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  ssindif0im  3551  mpteq1  4168  iinexgm  4238  exmid1stab  4292  mss  4312  eusv2nf  4547  eldifpw  4568  ordtriexmid  4613  onsucsssucexmid  4619  ordsucunielexmid  4623  nn0suc  4696  xpss1  4829  xpiindim  4859  reldm0  4941  elrnmpt1s  4974  resdm  5044  resid  5062  eliniseg  5098  trinxp  5122  inimasn  5146  ssrnres  5171  cnveq0  5185  coi2  5245  relrelss  5255  funcnvres  5394  funimaex  5406  fnresin1  5438  fnresin2  5439  fresin  5506  dffv3g  5625  ssimaex  5697  dmfco  5704  fvmpt  5713  fsn  5809  fsn2  5811  funop  5820  elabrex  5887  elabrexg  5888  f1elima  5903  2ndconst  6374  tposfun  6412  tpostpos2  6417  tfrexlem  6486  tfri3  6519  rdgruledefgg  6527  rdgss  6535  frecsuclem  6558  frecrdg  6560  oa0  6611  om0  6612  oei0  6613  oav2  6617  oa1suc  6621  nnmsucr  6642  nnm1  6679  nnm2  6680  ecelqsg  6743  ecidg  6754  xpider  6761  qsel  6767  mapdm0  6818  map0e  6841  mapsnconst  6849  ixpsnf1o  6891  map1  6973  dom1o  6985  xp1en  6990  xpcomco  6993  xpmapenlem  7018  findcard2s  7060  findcard2d  7061  findcard2sd  7062  exmidpw  7078  residfi  7115  fidcenumlemr  7130  sbthlem7  7138  eqinfti  7195  djueq1  7215  omp1eomlem  7269  endjusym  7271  eninl  7272  eninr  7273  difinfsn  7275  finomni  7315  pm54.43  7371  exmidonfinlem  7379  2onetap  7449  mulidpi  7513  nlt1pig  7536  indpi  7537  halfnqq  7605  archnqq  7612  prarloclemarch  7613  prarloclemarch2  7614  nnnq  7617  nq0a0  7652  addpinq1  7659  prarloclemlt  7688  prarloclemlo  7689  prarloclem3  7692  prarloclemcalc  7697  nqprm  7737  addnqpr1  7757  1idprl  7785  1idpru  7786  1idpr  7787  recexprlem1ssl  7828  recexprlem1ssu  7829  ltmprr  7837  0idsr  7962  1idsr  7963  00sr  7964  pn0sr  7966  negexsr  7967  recexgt0sr  7968  ltm1sr  7972  archsr  7977  prsrcl  7979  prsradd  7981  mappsrprg  7999  map2psrprg  8000  elrealeu  8024  pitonnlem1p1  8041  peano2nnnn  8048  ax1rid  8072  axcnre  8076  peano5nnnn  8087  peano2cn  8289  peano2re  8290  addlid  8293  subid  8373  subid1  8374  negid  8401  negeq0  8408  peano2cnm  8420  peano2rem  8421  mul01  8543  lt0neg1  8623  le0neg1  8625  recexre  8733  inelr  8739  rimul  8740  reapmul1  8750  apsqgt0  8756  mulge0  8774  negap0  8785  divvalap  8829  rerecclap  8885  div2negap  8890  divgt0i2i  9072  peano5nni  9121  nnge1  9141  times2  9247  addltmul  9356  nn0p1nn  9416  peano2nn0  9417  nn0lele2xi  9428  znnnlt1  9502  nn0lt10b  9535  prime  9554  msqznn  9555  zeo  9560  elnn1uz2  9810  qreccl  9845  qdivcl  9846  irrmul  9850  rphalfcl  9885  rpnegap  9890  zgt1rpn0n1  9899  ltpnf  9984  nltmnf  9992  pnfge  9993  xlt0neg1  10042  xle0neg1  10044  xaddpnf1  10050  xaddmnf1  10052  xaddid1  10066  xsubge0  10085  xleaddadd  10091  elioopnf  10171  elicopnf  10173  iccshftri  10199  iccshftli  10201  iccdili  10203  icccntri  10205  fzprval  10286  fzofzp1  10441  fzostep1  10451  flqge0nn0  10521  flqge1nn  10522  fldiv4p1lem1div2  10533  exp1  10775  qexpclz  10790  nn0sqcl  10796  expeq0  10800  expubnd  10826  sqval  10827  sqeq0  10832  resqcl  10837  zsqcl  10840  iexpcyc  10874  binom21  10882  bcnn  10987  bcn2  10994  bcn2p1  11000  bcnm1  11002  fihasheq0  11023  hashsng  11028  fihashen1  11029  fimaxq  11057  iswrddm0  11103  ccatval2  11141  ccatsymb  11145  ccatrid  11150  eqs1  11169  s111  11172  swrdnd  11199  pfx00g  11215  shftfibg  11339  shftfib  11342  reim0  11380  imval2  11413  cjap0  11426  cjne0  11427  rexuz3  11509  resqrexlemover  11529  abssq  11600  nn0abscl  11604  nnabscl  11619  abs2dif  11625  max0addsup  11738  climshft  11823  bcxmas  12008  efgt1p2  12214  efgt1p  12215  efi4p  12236  resin4p  12237  recos4p  12238  sinbnd  12271  cosbnd  12272  dvdsval2  12309  zdvdsdc  12331  dvdsmul2  12333  dvdsmulcr  12340  dvdsabseq  12366  divconjdvds  12368  alzdvds  12373  fzo0dvdseq  12376  odd2np1lem  12391  mod2eq1n2dvds  12398  flodddiv4  12455  flodddiv4t2lthalf  12458  bits0  12467  bitsp1o  12472  gcdmndc  12484  gcd0id  12508  gcd1  12516  dfgcd2  12543  gcdmultiple  12549  gcdmultiplez  12550  dvdssq  12560  lcmmndc  12592  lcm0val  12595  dvdslcm  12599  lcmeq0  12601  lcmgcd  12608  lcmdvds  12609  lcmid  12610  lcm1  12611  cncongr2  12634  isprm3  12648  prm2orodd  12656  sqrt2irrap  12710  phiprm  12753  pc0  12835  pcxqcl  12843  pcdvdstr  12858  unennn  12976  ennnfonelemim  13003  ctinfom  13007  ctinf  13009  enctlem  13011  elrestr  13288  tgval  13303  tgvalex  13304  xpsfrnel  13385  xpsfeq  13386  xpscf  13388  mulg1  13674  mulgnegnn  13677  ghmghmrn  13808  subrngintm  14184  subrgintm  14215  lsp0  14395  mulgrhm2  14582  zlmlemg  14600  zlmsca  14604  0opn  14688  topopn  14690  0cld  14794  ntropn  14799  ntrtop  14810  ntr0  14816  neipsm  14836  rest0  14861  xmetres  15064  metres  15065  mopnex  15187  tgioo  15236  cnlimcim  15353  cnlimc  15354  dvfre  15392  dveflem  15408  dvef  15409  efcn  15450  sin2pim  15495  cos2pim  15496  sinmpi  15497  cosmpi  15498  sinppi  15499  cosppi  15500  efimpi  15501  sincosq1lem  15507  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  sinq34lt0t  15513  sincosq1eq  15521  abssinper  15528  logrpap0b  15558  loglt1b  15575  rpcxp0  15580  rpcxp1  15581  rpcxpsqrt  15604  logsqrt  15605  rprelogbdiv  15639  lgs0  15700  lgs2  15704  lgsneg  15711  lgsdilem  15714  lgsdir2lem2  15716  lgsdir2lem4  15718  lgsdir2lem5  15719  lgsne0  15725  2lgslem1a2  15774  2lgslem1c  15777  upgr0eop  15930  uspgrushgr  15986  usgruspgr  15989  wlklenvclwlk  16094  upgr2wlkdc  16096  bj-inf2vnlem1  16357  pwle2  16393  pwf1oexmid  16394  domomsubct  16396  nninfsellemeqinf  16412  sbthom  16424  iswomninnlem  16447  redc0  16455