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  1366  equs4  1773  sb4bor  1884  elvd  2820  eueq2dc  2993  sbcgf  3113  csbconstgf  3154  sbcnestg  3195  csbnestg  3196  csbnest1g  3197  ssindif0im  3572  mpteq1  4199  iinexgm  4271  exmid1stab  4326  mss  4347  eusv2nf  4582  eldifpw  4603  ordtriexmid  4648  onsucsssucexmid  4654  ordsucunielexmid  4658  nn0suc  4731  xpss1  4865  xpiindim  4897  reldm0  4979  elrnmpt1s  5012  resdm  5082  resid  5100  eliniseg  5137  trinxp  5161  inimasn  5185  ssrnres  5210  cnveq0  5224  coi2  5284  relrelss  5294  funcnvres  5434  funimaex  5446  fnresin1  5478  fnresin2  5479  fresin  5548  dffv3g  5671  ssimaex  5743  dmfco  5750  fvmpt  5759  fsn  5854  fsn2  5856  funop  5866  elabrex  5936  elabrexg  5937  f1elima  5952  2ndconst  6431  tposfun  6504  tpostpos2  6509  tfrexlem  6578  tfri3  6611  rdgruledefgg  6619  rdgss  6627  frecsuclem  6650  frecrdg  6652  oa0  6703  om0  6704  oei0  6705  oav2  6709  oa1suc  6713  nnmsucr  6734  nnm1  6771  nnm2  6772  ecelqsg  6835  ecidg  6846  xpider  6853  qsel  6859  mapdm0  6910  map0e  6933  mapsnconst  6942  ixpsnf1o  6984  map1  7067  dom1o  7082  xp1en  7087  xpcomco  7090  xpmapenlem  7115  findcard2s  7160  findcard2d  7161  findcard2sd  7162  exmidpw  7181  residfi  7220  fidcenumlemr  7238  sbthlem7  7246  eqinfti  7324  djueq1  7344  omp1eomlem  7398  endjusym  7400  eninl  7401  eninr  7402  difinfsn  7404  finomni  7444  pm54.43  7500  exmidonfinlem  7509  2onetap  7585  mulidpi  7649  nlt1pig  7672  indpi  7673  halfnqq  7741  archnqq  7748  prarloclemarch  7749  prarloclemarch2  7750  nnnq  7753  nq0a0  7788  addpinq1  7795  prarloclemlt  7824  prarloclemlo  7825  prarloclem3  7828  prarloclemcalc  7833  nqprm  7873  addnqpr1  7893  1idprl  7921  1idpru  7922  1idpr  7923  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  0idsr  8098  1idsr  8099  00sr  8100  pn0sr  8102  negexsr  8103  recexgt0sr  8104  ltm1sr  8108  archsr  8113  prsrcl  8115  prsradd  8117  mappsrprg  8135  map2psrprg  8136  elrealeu  8160  pitonnlem1p1  8177  peano2nnnn  8184  ax1rid  8208  axcnre  8212  peano5nnnn  8223  peano2cn  8424  peano2re  8425  addlid  8428  subid  8508  subid1  8509  negid  8536  negeq0  8543  peano2cnm  8555  peano2rem  8556  mul01  8679  lt0neg1  8759  le0neg1  8761  recexre  8869  inelr  8875  rimul  8876  reapmul1  8886  apsqgt0  8892  mulge0  8910  negap0  8921  divvalap  8965  rerecclap  9021  div2negap  9026  divgt0i2i  9208  peano5nni  9257  nnge1  9277  times2  9383  addltmul  9492  nn0p1nn  9552  peano2nn0  9553  nn0lele2xi  9564  fcdmnn0supp  9565  fcdmnn0fsupp  9566  fcdmnn0suppg  9567  znnnlt1  9642  nn0lt10b  9676  prime  9695  msqznn  9696  zeo  9701  elnn1uz2  9957  qreccl  9992  qdivcl  9993  irrmul  9997  rphalfcl  10032  rpnegap  10037  zgt1rpn0n1  10046  ltpnf  10132  nltmnf  10140  pnfge  10141  xlt0neg1  10190  xle0neg1  10192  xaddpnf1  10198  xaddmnf1  10200  xaddid1  10214  xsubge0  10233  xleaddadd  10239  elioopnf  10319  elicopnf  10321  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  fzprval  10438  fzofzp1  10594  fzostep1  10605  flqge0nn0  10677  flqge1nn  10678  fldiv4p1lem1div2  10689  exp1  10931  qexpclz  10946  nn0sqcl  10952  expeq0  10956  expubnd  10982  sqval  10983  sqeq0  10988  resqcl  10993  zsqcl  10996  iexpcyc  11030  binom21  11038  bcnn  11144  bcn2  11151  bcn2p1  11158  bcnm1  11160  fihasheq0  11181  hashsng  11186  fihashen1  11187  fimaxq  11219  iswrddm0  11273  ccatval2  11311  ccatsymb  11315  ccatrid  11320  eqs1  11341  s111  11344  swrdnd  11376  pfx00g  11392  shftfibg  11530  shftfib  11533  reim0  11571  imval2  11604  cjap0  11617  cjne0  11618  rexuz3  11700  resqrexlemover  11720  abssq  11791  nn0abscl  11795  nnabscl  11810  abs2dif  11816  max0addsup  11929  climshft  12014  bcxmas  12200  efgt1p2  12406  efgt1p  12407  efi4p  12428  resin4p  12429  recos4p  12430  sinbnd  12463  cosbnd  12464  dvdsval2  12501  zdvdsdc  12523  dvdsmul2  12525  dvdsmulcr  12532  dvdsabseq  12558  divconjdvds  12560  alzdvds  12565  fzo0dvdseq  12568  odd2np1lem  12583  mod2eq1n2dvds  12590  flodddiv4  12647  flodddiv4t2lthalf  12650  bits0  12659  bitsp1o  12664  gcdmndc  12676  gcd0id  12700  gcd1  12708  dfgcd2  12735  gcdmultiple  12741  gcdmultiplez  12742  dvdssq  12752  lcmmndc  12784  lcm0val  12787  dvdslcm  12791  lcmeq0  12793  lcmgcd  12800  lcmdvds  12801  lcmid  12802  lcm1  12803  cncongr2  12826  isprm3  12840  prm2orodd  12848  sqrt2irrap  12902  phiprm  12945  pc0  13027  pcxqcl  13035  pcdvdstr  13050  ballotfilem2  13172  ballotfilemfcc  13177  ballotfilem4  13185  unennn  13232  ennnfonelemim  13259  ctinfom  13263  ctinf  13265  enctlem  13267  elrestr  13544  tgval  13559  tgvalex  13560  xpsfrnel  13641  xpsfeq  13642  xpscf  13644  mulg1  13930  mulgnegnn  13933  ghmghmrn  14064  subrngintm  14443  subrgintm  14474  lsp0  14683  mulgrhm2  14870  zlmlemg  14888  zlmsca  14892  0opn  14983  topopn  14985  0cld  15089  ntropn  15094  ntrtop  15105  ntr0  15111  neipsm  15131  rest0  15156  xmetres  15359  metres  15360  mopnex  15482  tgioo  15531  cnlimcim  15648  cnlimc  15649  dvfre  15687  dveflem  15703  dvef  15704  efcn  15745  sin2pim  15790  cos2pim  15791  sinmpi  15792  cosmpi  15793  sinppi  15794  cosppi  15795  efimpi  15796  sincosq1lem  15802  sincosq2sgn  15804  sincosq3sgn  15805  sincosq4sgn  15806  sinq12gt0  15807  sinq34lt0t  15808  sincosq1eq  15816  abssinper  15823  logrpap0b  15853  loglt1b  15870  rpcxp0  15875  rpcxp1  15876  rpcxpsqrt  15899  logsqrt  15900  rprelogbdiv  15934  lgs0  15998  lgs2  16002  lgsneg  16009  lgsdilem  16012  lgsdir2lem2  16014  lgsdir2lem4  16016  lgsdir2lem5  16017  lgsne0  16023  2lgslem1a2  16072  2lgslem1c  16075  upgr0eop  16229  uspgrushgr  16287  usgruspgr  16290  usgr0eop  16349  0grsubgr  16371  wlklenvclwlk  16480  upgr2wlkdc  16484  clwwlk0on0  16538  konigsbergssiedgwen  16593  bj-inf2vnlem1  16852  pwle2  16884  pwf1oexmid  16885  domomsubct  16887  nninfsellemeqinf  16906  sbthom  16918  qdiff  16945  iswomninnlem  16946  redc0  16954