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  4215  iinexgm  4290  exmid1stab  4345  mss  4366  eusv2nf  4602  eldifpw  4623  ordtriexmid  4668  onsucsssucexmid  4674  ordsucunielexmid  4678  nn0suc  4751  xpss1  4885  xpiindim  4917  reldm0  4999  elrnmpt1s  5032  resdm  5102  resid  5120  eliniseg  5157  trinxp  5181  inimasn  5205  ssrnres  5230  cnveq0  5244  coi2  5304  relrelss  5314  funcnvres  5454  funimaex  5466  fnresin1  5498  fnresin2  5499  fresin  5568  dffv3g  5691  ssimaex  5764  dmfco  5773  fvmpt  5782  fsn  5880  fsn2  5882  funop  5892  elabrex  5963  elabrexg  5964  f1elima  5979  2ndconst  6458  tposfun  6531  tpostpos2  6536  tfrexlem  6605  tfri3  6638  rdgruledefgg  6646  rdgss  6654  frecsuclem  6677  frecrdg  6679  oa0  6730  om0  6731  oei0  6732  oav2  6736  oa1suc  6740  nnmsucr  6761  nnm1  6798  nnm2  6799  ecelqsg  6862  ecidg  6873  xpider  6880  qsel  6886  mapdm0  6937  map0e  6967  mapsnconst  6976  ixpsnf1o  7018  map1  7101  dom1o  7116  xp1en  7121  xpcomco  7124  xpmapenlem  7149  findcard2s  7194  findcard2d  7195  findcard2sd  7196  exmidpw  7215  residfi  7254  fidcenumlemr  7272  sbthlem7  7280  eqinfti  7360  djueq1  7380  omp1eomlem  7434  endjusym  7436  eninl  7437  eninr  7438  difinfsn  7440  finomni  7480  pm54.43  7536  exmidonfinlem  7545  2onetap  7621  mulidpi  7685  nlt1pig  7708  indpi  7709  halfnqq  7777  archnqq  7784  prarloclemarch  7785  prarloclemarch2  7786  nnnq  7789  nq0a0  7824  addpinq1  7831  prarloclemlt  7860  prarloclemlo  7861  prarloclem3  7864  prarloclemcalc  7869  nqprm  7909  addnqpr1  7929  1idprl  7957  1idpru  7958  1idpr  7959  recexprlem1ssl  8000  recexprlem1ssu  8001  ltmprr  8009  0idsr  8134  1idsr  8135  00sr  8136  pn0sr  8138  negexsr  8139  recexgt0sr  8140  ltm1sr  8144  archsr  8149  prsrcl  8151  prsradd  8153  mappsrprg  8171  map2psrprg  8172  elrealeu  8196  pitonnlem1p1  8213  peano2nnnn  8220  ax1rid  8244  axcnre  8248  peano5nnnn  8259  peano2cn  8461  peano2re  8462  addlid  8465  subid  8545  subid1  8546  negid  8573  negeq0  8580  peano2cnm  8592  peano2rem  8593  mul01  8716  lt0neg1  8796  le0neg1  8798  recexre  8907  inelr  8913  rimul  8914  reapmul1  8924  apsqgt0  8930  mulge0  8948  negap0  8959  divvalap  9005  rerecclap  9061  div2negap  9066  divgt0i2i  9248  indconst0  9303  indconst1  9304  peano5nni  9308  nnge1  9328  times2  9434  addltmul  9544  nn0p1nn  9604  peano2nn0  9605  nn0lele2xi  9616  fcdmnn0supp  9617  fcdmnn0fsupp  9618  fcdmnn0suppg  9619  znnnlt1  9694  nn0lt10b  9728  prime  9747  msqznn  9748  zeo  9753  elnn1uz2  10009  qreccl  10044  qdivcl  10045  irrmul  10049  rphalfcl  10084  rpnegap  10089  zgt1rpn0n1  10098  ltpnf  10184  nltmnf  10192  pnfge  10193  xlt0neg1  10242  xle0neg1  10244  xaddpnf1  10250  xaddmnf1  10252  xaddid1  10266  xsubge0  10285  xleaddadd  10291  elioopnf  10371  elicopnf  10373  iccshftri  10399  iccshftli  10401  iccdili  10403  icccntri  10405  fzprval  10491  fzofzp1  10647  fzostep1  10658  flqge0nn0  10730  flqge1nn  10731  fldiv4p1lem1div2  10742  exp1  10984  qexpclz  10999  nn0sqcl  11005  expeq0  11009  expubnd  11035  sqval  11036  sqeq0  11041  resqcl  11046  zsqcl  11049  iexpcyc  11083  binom21  11091  bcnn  11197  bcn2  11204  bcn2p1  11211  bcnm1  11213  fihasheq0  11234  hashsng  11239  fihashen1  11240  fimaxq  11272  hashf1lem2  11288  iswrddm0  11330  ccatval2  11368  ccatsymb  11372  ccatrid  11377  eqs1  11398  s111  11401  swrdnd  11433  pfx00g  11449  shftfibg  11587  shftfib  11590  reim0  11628  imval2  11661  cjap0  11675  cjne0  11676  rexuz3  11758  resqrexlemover  11778  abssq  11849  nn0abscl  11853  nnabscl  11868  abs2dif  11874  max0addsup  11987  climshft  12072  bcxmas  12258  efgt1p2  12464  efgt1p  12465  efi4p  12486  resin4p  12487  recos4p  12488  sinbnd  12521  cosbnd  12522  dvdsval2  12559  zdvdsdc  12581  dvdsmul2  12583  dvdsmulcr  12590  dvdsabseq  12616  divconjdvds  12618  alzdvds  12623  fzo0dvdseq  12626  odd2np1lem  12641  mod2eq1n2dvds  12648  flodddiv4  12705  flodddiv4t2lthalf  12708  bits0  12717  bitsp1o  12722  gcdmndc  12734  gcd0id  12758  gcd1  12766  dfgcd2  12793  gcdmultiple  12799  gcdmultiplez  12800  dvdssq  12810  lcmmndc  12842  lcm0val  12845  dvdslcm  12849  lcmeq0  12851  lcmgcd  12858  lcmdvds  12859  lcmid  12860  lcm1  12861  cncongr2  12884  isprm3  12898  prm2orodd  12906  sqrt2irrap  12960  phiprm  13003  pc0  13085  pcxqcl  13093  pcdvdstr  13108  ballotfilem2  13230  ballotfilemfcc  13235  ballotfilem4  13243  unennn  13290  ennnfonelemim  13317  ctinfom  13321  ctinf  13323  enctlem  13325  elrestr  13603  tgval  13618  tgvalex  13619  xpsfrnel  13667  xpsfeq  13668  xpscf  13670  mulg1  13934  mulgnegnn  13937  ghmghmrn  14068  gsumconstcmn  14168  subrngintm  14522  subrgintm  14553  lsp0  14762  mulgrhm2  14947  zlmlemg  14965  zlmsca  14969  0opn  15109  topopn  15111  0cld  15215  ntropn  15220  ntrtop  15231  ntr0  15237  neipsm  15257  rest0  15282  xmetres  15485  metres  15486  mopnex  15608  tgioo  15657  cnlimcim  15774  cnlimc  15775  dvfre  15813  dveflem  15829  dvef  15830  efcn  15871  efap1p  15882  sin2pim  15917  cos2pim  15918  sinmpi  15919  cosmpi  15920  sinppi  15921  cosppi  15922  efimpi  15923  sincosq1lem  15929  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  sinq34lt0t  15935  sincosq1eq  15943  abssinper  15950  logrpap0b  15981  loglt1b  15998  rpcxp0  16006  rpcxp1  16007  rpcxpsqrt  16030  logsqrt  16031  rprelogbdiv  16065  lgs0  16144  lgs2  16148  lgsneg  16155  lgsdilem  16158  lgsdir2lem2  16160  lgsdir2lem4  16162  lgsdir2lem5  16163  lgsne0  16169  2lgslem1a2  16218  2lgslem1c  16221  upgr0eop  16375  uspgrushgr  16433  usgruspgr  16436  usgr0eop  16495  0grsubgr  16517  wlklenvclwlk  16626  upgr2wlkdc  16630  clwwlk0on0  16684  konigsbergssiedgwen  16739  bj-inf2vnlem1  17008  pwle2  17040  pwf1oexmid  17041  domomsubct  17043  nninfsellemeqinf  17071  sbthom  17083  qdiff  17110  iswomninnlem  17111  redc0  17119