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  1340  equs4  1736  sb4bor  1846  elvd  2757  eueq2dc  2925  sbcgf  3045  csbconstgf  3085  sbcnestg  3125  csbnestg  3126  csbnest1g  3127  ssindif0im  3497  mpteq1  4102  iinexgm  4172  exmid1stab  4226  mss  4244  eusv2nf  4474  eldifpw  4495  ordtriexmid  4538  onsucsssucexmid  4544  ordsucunielexmid  4548  nn0suc  4621  xpss1  4754  xpiindim  4782  reldm0  4863  elrnmpt1s  4895  resdm  4964  resid  4982  eliniseg  5016  trinxp  5040  inimasn  5064  ssrnres  5089  cnveq0  5103  coi2  5163  relrelss  5173  funcnvres  5308  funimaex  5320  fnresin1  5349  fnresin2  5350  fresin  5413  dffv3g  5530  ssimaex  5598  dmfco  5605  fvmpt  5614  fsn  5709  fsn2  5711  elabrex  5779  elabrexg  5780  f1elima  5795  2ndconst  6248  tposfun  6286  tpostpos2  6291  tfrexlem  6360  tfri3  6393  rdgruledefgg  6401  rdgss  6409  frecsuclem  6432  frecrdg  6434  oa0  6483  om0  6484  oei0  6485  oav2  6489  oa1suc  6493  nnmsucr  6514  nnm1  6551  nnm2  6552  ecelqsg  6615  ecidg  6626  xpider  6633  qsel  6639  mapdm0  6690  map0e  6713  mapsnconst  6721  ixpsnf1o  6763  map1  6839  xp1en  6850  xpcomco  6853  xpmapenlem  6878  findcard2s  6919  findcard2d  6920  findcard2sd  6921  exmidpw  6937  fidcenumlemr  6985  sbthlem7  6993  eqinfti  7050  djueq1  7070  omp1eomlem  7124  endjusym  7126  eninl  7127  eninr  7128  difinfsn  7130  finomni  7169  pm54.43  7220  exmidonfinlem  7223  2onetap  7285  mulidpi  7348  nlt1pig  7371  indpi  7372  halfnqq  7440  archnqq  7447  prarloclemarch  7448  prarloclemarch2  7449  nnnq  7452  nq0a0  7487  addpinq1  7494  prarloclemlt  7523  prarloclemlo  7524  prarloclem3  7527  prarloclemcalc  7532  nqprm  7572  addnqpr1  7592  1idprl  7620  1idpru  7621  1idpr  7622  recexprlem1ssl  7663  recexprlem1ssu  7664  ltmprr  7672  0idsr  7797  1idsr  7798  00sr  7799  pn0sr  7801  negexsr  7802  recexgt0sr  7803  ltm1sr  7807  archsr  7812  prsrcl  7814  prsradd  7816  mappsrprg  7834  map2psrprg  7835  elrealeu  7859  pitonnlem1p1  7876  peano2nnnn  7883  ax1rid  7907  axcnre  7911  peano5nnnn  7922  peano2cn  8123  peano2re  8124  addlid  8127  subid  8207  subid1  8208  negid  8235  negeq0  8242  peano2cnm  8254  peano2rem  8255  mul01  8377  lt0neg1  8456  le0neg1  8458  recexre  8566  inelr  8572  rimul  8573  reapmul1  8583  apsqgt0  8589  mulge0  8607  negap0  8618  divvalap  8662  rerecclap  8718  div2negap  8723  divgt0i2i  8905  peano5nni  8953  nnge1  8973  times2  9079  addltmul  9186  nn0p1nn  9246  peano2nn0  9247  nn0lele2xi  9258  znnnlt1  9332  nn0lt10b  9364  prime  9383  msqznn  9384  zeo  9389  elnn1uz2  9639  qreccl  9674  qdivcl  9675  irrmul  9679  rphalfcl  9713  rpnegap  9718  zgt1rpn0n1  9727  ltpnf  9812  nltmnf  9820  pnfge  9821  xlt0neg1  9870  xle0neg1  9872  xaddpnf1  9878  xaddmnf1  9880  xaddid1  9894  xsubge0  9913  xleaddadd  9919  elioopnf  9999  elicopnf  10001  iccshftri  10027  iccshftli  10029  iccdili  10031  icccntri  10033  fzprval  10114  fzofzp1  10259  fzostep1  10269  flqge0nn0  10326  flqge1nn  10327  fldiv4p1lem1div2  10338  exp1  10560  qexpclz  10575  nn0sqcl  10581  expeq0  10585  expubnd  10611  sqval  10612  sqeq0  10617  resqcl  10622  zsqcl  10625  iexpcyc  10659  binom21  10667  bcnn  10772  bcn2  10779  bcn2p1  10785  bcnm1  10787  fihasheq0  10808  hashsng  10813  fihashen1  10814  fimaxq  10842  shftfibg  10864  shftfib  10867  reim0  10905  imval2  10938  cjap0  10951  cjne0  10952  rexuz3  11034  resqrexlemover  11054  abssq  11125  nn0abscl  11129  nnabscl  11144  abs2dif  11150  max0addsup  11263  climshft  11347  bcxmas  11532  efgt1p2  11738  efgt1p  11739  efi4p  11760  resin4p  11761  recos4p  11762  sinbnd  11795  cosbnd  11796  dvdsval2  11832  zdvdsdc  11854  dvdsmul2  11856  dvdsmulcr  11863  dvdsabseq  11888  divconjdvds  11890  alzdvds  11895  fzo0dvdseq  11898  odd2np1lem  11912  mod2eq1n2dvds  11919  flodddiv4  11974  flodddiv4t2lthalf  11977  gcdmndc  11980  gcd0id  12015  gcd1  12023  dfgcd2  12050  gcdmultiple  12056  gcdmultiplez  12057  dvdssq  12067  lcmmndc  12097  lcm0val  12100  dvdslcm  12104  lcmeq0  12106  lcmgcd  12113  lcmdvds  12114  lcmid  12115  lcm1  12116  cncongr2  12139  isprm3  12153  prm2orodd  12161  sqrt2irrap  12215  phiprm  12258  pc0  12339  pcxqcl  12347  pcdvdstr  12362  unennn  12451  ennnfonelemim  12478  ctinfom  12482  ctinf  12484  enctlem  12486  elrestr  12755  tgval  12770  tgvalex  12771  xpsfrnel  12823  xpsfeq  12824  xpscf  12826  mulg1  13086  mulgnegnn  13089  ghmghmrn  13219  subrngintm  13576  subrgintm  13607  lsp0  13756  mulgrhm2  13925  zlmlemg  13941  zlmsca  13945  0opn  13983  topopn  13985  0cld  14089  ntropn  14094  ntrtop  14105  ntr0  14111  neipsm  14131  rest0  14156  xmetres  14359  metres  14360  mopnex  14482  tgioo  14523  cnlimcim  14617  cnlimc  14618  dvfre  14651  dveflem  14664  dvef  14665  efcn  14666  sin2pim  14711  cos2pim  14712  sinmpi  14713  cosmpi  14714  sinppi  14715  cosppi  14716  efimpi  14717  sincosq1lem  14723  sincosq2sgn  14725  sincosq3sgn  14726  sincosq4sgn  14727  sinq12gt0  14728  sinq34lt0t  14729  sincosq1eq  14737  abssinper  14744  logrpap0b  14774  loglt1b  14791  rpcxp0  14796  rpcxp1  14797  rpcxpsqrt  14819  logsqrt  14820  rprelogbdiv  14852  lgs0  14892  lgs2  14896  lgsneg  14903  lgsdilem  14906  lgsdir2lem2  14908  lgsdir2lem4  14910  lgsdir2lem5  14911  lgsne0  14917  bj-inf2vnlem1  15200  pwle2  15227  pwf1oexmid  15228  nninfsellemeqinf  15244  sbthom  15253  iswomninnlem  15276  redc0  15284