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  6980  ixpsnf1o  7022  map1  7105  dom1o  7120  xp1en  7125  xpcomco  7128  xpmapenlem  7153  findcard2s  7198  findcard2d  7199  findcard2sd  7200  exmidpw  7219  residfi  7258  fidcenumlemr  7277  sbthlem7  7285  eqinfti  7366  djueq1  7386  omp1eomlem  7440  endjusym  7442  eninl  7443  eninr  7444  difinfsn  7446  finomni  7486  pm54.43  7542  exmidonfinlem  7551  2onetap  7627  mulidpi  7691  nlt1pig  7714  indpi  7715  halfnqq  7783  archnqq  7790  prarloclemarch  7791  prarloclemarch2  7792  nnnq  7795  nq0a0  7830  addpinq1  7837  prarloclemlt  7866  prarloclemlo  7867  prarloclem3  7870  prarloclemcalc  7875  nqprm  7915  addnqpr1  7935  1idprl  7963  1idpru  7964  1idpr  7965  recexprlem1ssl  8006  recexprlem1ssu  8007  ltmprr  8015  0idsr  8140  1idsr  8141  00sr  8142  pn0sr  8144  negexsr  8145  recexgt0sr  8146  ltm1sr  8150  archsr  8155  prsrcl  8157  prsradd  8159  mappsrprg  8177  map2psrprg  8178  elrealeu  8202  pitonnlem1p1  8219  peano2nnnn  8226  ax1rid  8250  axcnre  8254  peano5nnnn  8265  peano2cn  8468  peano2re  8469  addlid  8472  subid  8552  subid1  8553  negid  8580  negeq0  8587  peano2cnm  8599  peano2rem  8600  mul01  8723  lt0neg1  8803  le0neg1  8805  recexre  8914  inelr  8920  rimul  8921  reapmul1  8931  apsqgt0  8937  mulge0  8955  negap0  8966  divvalap  9012  rerecclap  9068  div2negap  9073  divgt0i2i  9255  indconst0  9311  indconst1  9312  peano5nni  9316  nnge1  9336  times2  9442  addltmul  9553  nn0p1nn  9613  peano2nn0  9614  nn0lele2xi  9625  fcdmnn0supp  9626  fcdmnn0fsupp  9627  fcdmnn0suppg  9628  znnnlt1  9703  nn0lt10b  9737  prime  9756  msqznn  9757  zeo  9762  elnn1uz2  10023  qreccl  10058  qdivcl  10059  irrmul  10064  rphalfcl  10099  rpnegap  10104  zgt1rpn0n1  10113  ltpnf  10199  nltmnf  10207  pnfge  10208  xlt0neg1  10257  xle0neg1  10259  xaddpnf1  10265  xaddmnf1  10267  xaddid1  10281  xsubge0  10300  xleaddadd  10306  elioopnf  10386  elicopnf  10388  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  fzprval  10506  fzofzp1  10662  fzostep1  10673  flqge0nn0  10749  flqge1nn  10750  fldiv4p1lem1div2  10761  exp1  11003  qexpclz  11018  nn0sqcl  11024  expeq0  11028  expubnd  11054  sqval  11055  sqeq0  11060  resqcl  11065  zsqcl  11068  iexpcyc  11102  binom21  11110  bcnn  11217  bcn2  11224  bcn2p1  11231  bcnm1  11233  fihasheq0  11254  hashsng  11259  fihashen1  11260  fimaxq  11292  hashf1lem2  11308  iswrddm0  11350  ccatval2  11388  ccatsymb  11392  ccatrid  11397  eqs1  11418  s111  11421  swrdnd  11453  pfx00g  11469  shftfibg  11607  shftfib  11610  reim0  11648  imval2  11681  cjap0  11695  cjne0  11696  rexuz3  11778  resqrexlemover  11798  abssq  11870  nn0abscl  11874  nnabscl  11889  abs2dif  11895  max0addsup  12008  climshft  12095  bcxmas  12281  efgt1p2  12487  efgt1p  12488  efi4p  12509  resin4p  12510  recos4p  12511  sinbnd  12544  cosbnd  12545  dvdsval2  12582  zdvdsdc  12604  dvdsmul2  12606  dvdsmulcr  12613  dvdsabseq  12639  divconjdvds  12641  alzdvds  12646  fzo0dvdseq  12649  odd2np1lem  12664  mod2eq1n2dvds  12671  flodddiv4  12728  flodddiv4t2lthalf  12731  bits0  12740  bitsp1o  12745  gcdmndc  12757  gcd0id  12781  gcd1  12789  dfgcd2  12816  gcdmultiple  12822  gcdmultiplez  12823  dvdssq  12833  lcmmndc  12865  lcm0val  12868  dvdslcm  12872  lcmeq0  12874  lcmgcd  12881  lcmdvds  12882  lcmid  12883  lcm1  12884  cncongr2  12907  isprm3  12921  prm2orodd  12929  sqrt2irrap  12985  phiprm  13030  pc0  13112  pcxqcl  13120  pcdvdstr  13135  ballotfilem2  13286  ballotfilemfcc  13291  ballotfilem4  13299  unennn  13346  ennnfonelemim  13373  ctinfom  13377  ctinf  13379  enctlem  13381  elrestr  13660  tgval  13675  tgvalex  13676  xpsfrnel  13724  xpsfeq  13725  xpscf  13727  mulg1  13991  mulgnegnn  13994  ghmghmrn  14125  cntrnsg  14176  gsumconstcmn  14266  subrngintm  14629  subrgintm  14660  lsp0  14869  mulgrhm2  15054  zlmlemg  15072  zlmsca  15076  0opn  15229  topopn  15231  0cld  15335  ntropn  15340  ntrtop  15351  ntr0  15357  neipsm  15377  rest0  15402  xmetres  15605  metres  15606  mopnex  15728  tgioo  15777  cnlimcim  15894  cnlimc  15895  dvfre  15933  dveflem  15949  dvef  15950  efcn  15991  efap1p  16002  sin2pim  16037  cos2pim  16038  sinmpi  16039  cosmpi  16040  sinppi  16041  cosppi  16042  efimpi  16043  sincosq1lem  16049  sincosq2sgn  16051  sincosq3sgn  16052  sincosq4sgn  16053  sinq12gt0  16054  sinq34lt0t  16055  sincosq1eq  16063  abssinper  16070  logrpap0b  16103  loglt1b  16120  rpcxp0  16128  rpcxp1  16129  rpcxpsqrt  16154  logsqrt  16155  rprelogbdiv  16190  ppiqp1le  16264  ppiqeq0  16277  ppiublem1  16288  ppiqub  16290  chtqub  16293  lgs0  16334  lgs2  16338  lgsneg  16345  lgsdilem  16348  lgsdir2lem2  16350  lgsdir2lem4  16352  lgsdir2lem5  16353  lgsne0  16359  2lgslem1a2  16408  2lgslem1c  16411  upgr0eop  16565  uspgrushgr  16623  usgruspgr  16626  usgr0eop  16685  0grsubgr  16707  wlklenvclwlk  16816  upgr2wlkdc  16820  clwwlk0on0  16874  konigsbergssiedgwen  16929  bj-inf2vnlem1  17198  pwle2  17230  pwf1oexmid  17231  domomsubct  17233  nninfsellemeqinf  17262  sbthom  17274  qdiff  17302  iswomninnlem  17303  redc0  17311