Theorem mpan2 429

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 425	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  443  mp3an23  1370  equs4  1777  sb4bor  1888  elvd  2826  eueq2dc  2999  sbcgf  3119  csbconstgf  3160  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  ssindif0im  3584  mpteq1  4213  iinexgm  4288  exmid1stab  4343  mss  4364  eusv2nf  4600  eldifpw  4621  ordtriexmid  4666  onsucsssucexmid  4672  ordsucunielexmid  4676  nn0suc  4749  xpss1  4883  xpiindim  4915  reldm0  4997  elrnmpt1s  5030  resdm  5100  resid  5118  eliniseg  5155  trinxp  5179  inimasn  5203  ssrnres  5228  cnveq0  5242  coi2  5302  relrelss  5312  funcnvres  5452  funimaex  5464  fnresin1  5496  fnresin2  5497  fresin  5566  dffv3g  5689  ssimaex  5761  dmfco  5770  fvmpt  5779  fsn  5874  fsn2  5876  funop  5886  elabrex  5957  elabrexg  5958  f1elima  5973  2ndconst  6452  tposfun  6525  tpostpos2  6530  tfrexlem  6599  tfri3  6632  rdgruledefgg  6640  rdgss  6648  frecsuclem  6671  frecrdg  6673  oa0  6724  om0  6725  oei0  6726  oav2  6730  oa1suc  6734  nnmsucr  6755  nnm1  6792  nnm2  6793  ecelqsg  6856  ecidg  6867  xpider  6874  qsel  6880  mapdm0  6931  map0e  6961  mapsnconst  6970  ixpsnf1o  7012  map1  7095  dom1o  7110  xp1en  7115  xpcomco  7118  xpmapenlem  7143  findcard2s  7188  findcard2d  7189  findcard2sd  7190  exmidpw  7209  residfi  7248  fidcenumlemr  7266  sbthlem7  7274  eqinfti  7354  djueq1  7374  omp1eomlem  7428  endjusym  7430  eninl  7431  eninr  7432  difinfsn  7434  finomni  7474  pm54.43  7530  exmidonfinlem  7539  2onetap  7615  mulidpi  7679  nlt1pig  7702  indpi  7703  halfnqq  7771  archnqq  7778  prarloclemarch  7779  prarloclemarch2  7780  nnnq  7783  nq0a0  7818  addpinq1  7825  prarloclemlt  7854  prarloclemlo  7855  prarloclem3  7858  prarloclemcalc  7863  nqprm  7903  addnqpr1  7923  1idprl  7951  1idpru  7952  1idpr  7953  recexprlem1ssl  7994  recexprlem1ssu  7995  ltmprr  8003  0idsr  8128  1idsr  8129  00sr  8130  pn0sr  8132  negexsr  8133  recexgt0sr  8134  ltm1sr  8138  archsr  8143  prsrcl  8145  prsradd  8147  mappsrprg  8165  map2psrprg  8166  elrealeu  8190  pitonnlem1p1  8207  peano2nnnn  8214  ax1rid  8238  axcnre  8242  peano5nnnn  8253  peano2cn  8455  peano2re  8456  addlid  8459  subid  8539  subid1  8540  negid  8567  negeq0  8574  peano2cnm  8586  peano2rem  8587  mul01  8710  lt0neg1  8790  le0neg1  8792  recexre  8900  inelr  8906  rimul  8907  reapmul1  8917  apsqgt0  8923  mulge0  8941  negap0  8952  divvalap  8998  rerecclap  9054  div2negap  9059  divgt0i2i  9241  peano5nni  9290  nnge1  9310  times2  9416  addltmul  9525  nn0p1nn  9585  peano2nn0  9586  nn0lele2xi  9597  fcdmnn0supp  9598  fcdmnn0fsupp  9599  fcdmnn0suppg  9600  znnnlt1  9675  nn0lt10b  9709  prime  9728  msqznn  9729  zeo  9734  elnn1uz2  9990  qreccl  10025  qdivcl  10026  irrmul  10030  rphalfcl  10065  rpnegap  10070  zgt1rpn0n1  10079  ltpnf  10165  nltmnf  10173  pnfge  10174  xlt0neg1  10223  xle0neg1  10225  xaddpnf1  10231  xaddmnf1  10233  xaddid1  10247  xsubge0  10266  xleaddadd  10272  elioopnf  10352  elicopnf  10354  iccshftri  10380  iccshftli  10382  iccdili  10384  icccntri  10386  fzprval  10472  fzofzp1  10628  fzostep1  10639  flqge0nn0  10711  flqge1nn  10712  fldiv4p1lem1div2  10723  exp1  10965  qexpclz  10980  nn0sqcl  10986  expeq0  10990  expubnd  11016  sqval  11017  sqeq0  11022  resqcl  11027  zsqcl  11030  iexpcyc  11064  binom21  11072  bcnn  11178  bcn2  11185  bcn2p1  11192  bcnm1  11194  fihasheq0  11215  hashsng  11220  fihashen1  11221  fimaxq  11253  hashf1lem2  11269  iswrddm0  11311  ccatval2  11349  ccatsymb  11353  ccatrid  11358  eqs1  11379  s111  11382  swrdnd  11414  pfx00g  11430  shftfibg  11568  shftfib  11571  reim0  11609  imval2  11642  cjap0  11656  cjne0  11657  rexuz3  11739  resqrexlemover  11759  abssq  11830  nn0abscl  11834  nnabscl  11849  abs2dif  11855  max0addsup  11968  climshft  12053  bcxmas  12239  efgt1p2  12445  efgt1p  12446  efi4p  12467  resin4p  12468  recos4p  12469  sinbnd  12502  cosbnd  12503  dvdsval2  12540  zdvdsdc  12562  dvdsmul2  12564  dvdsmulcr  12571  dvdsabseq  12597  divconjdvds  12599  alzdvds  12604  fzo0dvdseq  12607  odd2np1lem  12622  mod2eq1n2dvds  12629  flodddiv4  12686  flodddiv4t2lthalf  12689  bits0  12698  bitsp1o  12703  gcdmndc  12715  gcd0id  12739  gcd1  12747  dfgcd2  12774  gcdmultiple  12780  gcdmultiplez  12781  dvdssq  12791  lcmmndc  12823  lcm0val  12826  dvdslcm  12830  lcmeq0  12832  lcmgcd  12839  lcmdvds  12840  lcmid  12841  lcm1  12842  cncongr2  12865  isprm3  12879  prm2orodd  12887  sqrt2irrap  12941  phiprm  12984  pc0  13066  pcxqcl  13074  pcdvdstr  13089  ballotfilem2  13211  ballotfilemfcc  13216  ballotfilem4  13224  unennn  13271  ennnfonelemim  13298  ctinfom  13302  ctinf  13304  enctlem  13306  elrestr  13584  tgval  13599  tgvalex  13600  xpsfrnel  13648  xpsfeq  13649  xpscf  13651  mulg1  13915  mulgnegnn  13918  ghmghmrn  14049  gsumconstcmn  14149  subrngintm  14503  subrgintm  14534  lsp0  14743  mulgrhm2  14928  zlmlemg  14946  zlmsca  14950  0opn  15090  topopn  15092  0cld  15196  ntropn  15201  ntrtop  15212  ntr0  15218  neipsm  15238  rest0  15263  xmetres  15466  metres  15467  mopnex  15589  tgioo  15638  cnlimcim  15755  cnlimc  15756  dvfre  15794  dveflem  15810  dvef  15811  efcn  15852  sin2pim  15897  cos2pim  15898  sinmpi  15899  cosmpi  15900  sinppi  15901  cosppi  15902  efimpi  15903  sincosq1lem  15909  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  sinq34lt0t  15915  sincosq1eq  15923  abssinper  15930  logrpap0b  15960  loglt1b  15977  rpcxp0  15983  rpcxp1  15984  rpcxpsqrt  16007  logsqrt  16008  rprelogbdiv  16042  lgs0  16115  lgs2  16119  lgsneg  16126  lgsdilem  16129  lgsdir2lem2  16131  lgsdir2lem4  16133  lgsdir2lem5  16134  lgsne0  16140  2lgslem1a2  16189  2lgslem1c  16192  upgr0eop  16346  uspgrushgr  16404  usgruspgr  16407  usgr0eop  16466  0grsubgr  16488  wlklenvclwlk  16597  upgr2wlkdc  16601  clwwlk0on0  16655  konigsbergssiedgwen  16710  bj-inf2vnlem1  16979  pwle2  17011  pwf1oexmid  17012  domomsubct  17014  nninfsellemeqinf  17033  sbthom  17045  qdiff  17072  iswomninnlem  17073  redc0  17081