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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used 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  4216  iinexgm  4292  exmid1stab  4347  mss  4368  eusv2nf  4604  eldifpw  4625  ordtriexmid  4670  onsucsssucexmid  4676  ordsucunielexmid  4680  nn0suc  4753  xpss1  4887  xpiindim  4919  reldm0  5001  elrnmpt1s  5034  resdm  5104  resid  5123  eliniseg  5160  trinxp  5184  inimasn  5208  ssrnres  5233  cnveq0  5247  coi2  5307  relrelss  5317  funcnvres  5457  funimaex  5469  fnresin1  5501  fnresin2  5502  fresin  5571  dffv3g  5694  ssimaex  5767  dmfco  5776  fvmpt  5785  fsn  5883  fsn2  5885  funop  5895  elabrex  5966  elabrexg  5967  f1elima  5982  2ndconst  6462  tposfun  6535  tpostpos2  6540  tfrexlem  6609  tfri3  6642  rdgruledefgg  6650  rdgss  6658  frecsuclem  6681  frecrdg  6683  oa0  6734  om0  6735  oei0  6736  oav2  6740  oa1suc  6744  nnmsucr  6765  nnm1  6802  nnm2  6803  ecelqsg  6866  ecidg  6877  xpider  6884  qsel  6890  mapdm0  6941  map0e  6971  mapsnconst  6981  ixpsnf1o  7023  map1  7106  dom1o  7121  xp1en  7126  xpcomco  7129  xpmapenlem  7154  findcard2s  7199  findcard2d  7200  findcard2sd  7201  exmidpw  7220  residfi  7259  fidcenumlemr  7278  sbthlem7  7286  eqinfti  7367  djueq1  7387  omp1eomlem  7441  endjusym  7443  eninl  7444  eninr  7445  difinfsn  7447  finomni  7487  pm54.43  7543  exmidonfinlem  7552  2onetap  7628  mulidpi  7692  nlt1pig  7715  indpi  7716  halfnqq  7784  archnqq  7791  prarloclemarch  7792  prarloclemarch2  7793  nnnq  7796  nq0a0  7831  addpinq1  7838  prarloclemlt  7867  prarloclemlo  7868  prarloclem3  7871  prarloclemcalc  7876  nqprm  7916  addnqpr1  7936  1idprl  7964  1idpru  7965  1idpr  7966  recexprlem1ssl  8007  recexprlem1ssu  8008  ltmprr  8016  0idsr  8141  1idsr  8142  00sr  8143  pn0sr  8145  negexsr  8146  recexgt0sr  8147  ltm1sr  8151  archsr  8156  prsrcl  8158  prsradd  8160  mappsrprg  8178  map2psrprg  8179  elrealeu  8203  pitonnlem1p1  8220  peano2nnnn  8227  ax1rid  8251  axcnre  8255  peano5nnnn  8266  peano2cn  8469  peano2re  8470  addlid  8473  subid  8553  subid1  8554  negid  8581  negeq0  8588  peano2cnm  8600  peano2rem  8601  mul01  8724  lt0neg1  8804  le0neg1  8806  recexre  8915  inelr  8921  rimul  8922  reapmul1  8932  apsqgt0  8938  mulge0  8956  negap0  8967  divvalap  9013  rerecclap  9069  div2negap  9074  divgt0i2i  9256  indconst0  9312  indconst1  9313  peano5nni  9317  nnge1  9337  times2  9443  addltmul  9554  nn0p1nn  9614  peano2nn0  9615  nn0lele2xi  9626  fcdmnn0supp  9627  fcdmnn0fsupp  9628  fcdmnn0suppg  9629  znnnlt1  9704  nn0lt10b  9738  prime  9757  msqznn  9758  zeo  9763  elnn1uz2  10024  qreccl  10059  qdivcl  10060  irrmul  10065  rphalfcl  10100  rpnegap  10105  zgt1rpn0n1  10114  ltpnf  10200  nltmnf  10208  pnfge  10209  xlt0neg1  10258  xle0neg1  10260  xaddpnf1  10266  xaddmnf1  10268  xaddid1  10282  xsubge0  10301  xleaddadd  10307  elioopnf  10387  elicopnf  10389  iccshftri  10415  iccshftli  10417  iccdili  10419  icccntri  10421  fzprval  10507  fzofzp1  10663  fzostep1  10674  flqge0nn0  10750  flqge1nn  10751  fldiv4p1lem1div2  10762  exp1  11004  qexpclz  11019  nn0sqcl  11025  expeq0  11029  expubnd  11055  sqval  11056  sqeq0  11061  resqcl  11066  zsqcl  11069  iexpcyc  11103  binom21  11111  bcnn  11218  bcn2  11225  bcn2p1  11232  bcnm1  11234  fihasheq0  11255  hashsng  11260  fihashen1  11261  fimaxq  11293  hashf1lem2  11309  iswrddm0  11351  ccatval2  11389  ccatsymb  11393  ccatrid  11398  eqs1  11419  s111  11422  swrdnd  11454  pfx00g  11470  shftfibg  11608  shftfib  11611  reim0  11649  imval2  11682  cjap0  11696  cjne0  11697  rexuz3  11779  resqrexlemover  11799  abssq  11871  nn0abscl  11875  nnabscl  11890  abs2dif  11896  max0addsup  12009  climshft  12096  bcxmas  12282  efgt1p2  12488  efgt1p  12489  efi4p  12510  resin4p  12511  recos4p  12512  sinbnd  12545  cosbnd  12546  dvdsval2  12583  zdvdsdc  12605  dvdsmul2  12607  dvdsmulcr  12614  dvdsabseq  12640  divconjdvds  12642  alzdvds  12647  fzo0dvdseq  12650  odd2np1lem  12665  mod2eq1n2dvds  12672  flodddiv4  12729  flodddiv4t2lthalf  12732  bits0  12741  bitsp1o  12746  gcdmndc  12758  gcd0id  12782  gcd1  12790  dfgcd2  12817  gcdmultiple  12823  gcdmultiplez  12824  dvdssq  12834  lcmmndc  12866  lcm0val  12869  dvdslcm  12873  lcmeq0  12875  lcmgcd  12882  lcmdvds  12883  lcmid  12884  lcm1  12885  cncongr2  12908  isprm3  12922  prm2orodd  12930  sqrt2irrap  12986  phiprm  13031  pc0  13113  pcxqcl  13121  pcdvdstr  13136  ballotfilem2  13287  ballotfilemfcc  13292  ballotfilem4  13300  unennn  13347  ennnfonelemim  13374  ctinfom  13378  ctinf  13380  enctlem  13382  elrestr  13661  tgval  13676  tgvalex  13677  xpsfrnel  13725  xpsfeq  13726  xpscf  13728  mulg1  13992  mulgnegnn  13995  ghmghmrn  14126  cntrnsg  14177  gsumconstcmn  14267  subrngintm  14630  subrgintm  14661  lsp0  14870  mulgrhm2  15055  zlmlemg  15073  zlmsca  15077  0opn  15244  topopn  15246  0cld  15350  ntropn  15355  ntrtop  15366  ntr0  15372  neipsm  15392  rest0  15417  xmetres  15620  metres  15621  mopnex  15743  tgioo  15792  cnlimcim  15909  cnlimc  15910  dvfre  15948  dveflem  15964  dvef  15965  efcn  16006  efap1p  16017  sin2pim  16052  cos2pim  16053  sinmpi  16054  cosmpi  16055  sinppi  16056  cosppi  16057  efimpi  16058  sincosq1lem  16064  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  sinq34lt0t  16070  sincosq1eq  16078  abssinper  16085  logrpap0b  16118  loglt1b  16135  rpcxp0  16143  rpcxp1  16144  rpcxpsqrt  16169  logsqrt  16170  rprelogbdiv  16205  ppiqp1le  16279  ppiqeq0  16292  ppiublem1  16303  ppiqub  16305  chtqub  16308  lgs0  16349  lgs2  16353  lgsneg  16360  lgsdilem  16363  lgsdir2lem2  16365  lgsdir2lem4  16367  lgsdir2lem5  16368  lgsne0  16374  2lgslem1a2  16423  2lgslem1c  16426  upgr0eop  16580  uspgrushgr  16638  usgruspgr  16641  usgr0eop  16700  0grsubgr  16722  wlklenvclwlk  16831  upgr2wlkdc  16835  clwwlk0on0  16889  konigsbergssiedgwen  16944  bj-inf2vnlem1  17213  pwle2  17245  pwf1oexmid  17246  domomsubct  17248  nninfsellemeqinf  17277  sbthom  17289  qdiff  17317  iswomninnlem  17318  redc0  17326