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  7361  djueq1  7381  omp1eomlem  7435  endjusym  7437  eninl  7438  eninr  7439  difinfsn  7441  finomni  7481  pm54.43  7537  exmidonfinlem  7546  2onetap  7622  mulidpi  7686  nlt1pig  7709  indpi  7710  halfnqq  7778  archnqq  7785  prarloclemarch  7786  prarloclemarch2  7787  nnnq  7790  nq0a0  7825  addpinq1  7832  prarloclemlt  7861  prarloclemlo  7862  prarloclem3  7865  prarloclemcalc  7870  nqprm  7910  addnqpr1  7930  1idprl  7958  1idpru  7959  1idpr  7960  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  0idsr  8135  1idsr  8136  00sr  8137  pn0sr  8139  negexsr  8140  recexgt0sr  8141  ltm1sr  8145  archsr  8150  prsrcl  8152  prsradd  8154  mappsrprg  8172  map2psrprg  8173  elrealeu  8197  pitonnlem1p1  8214  peano2nnnn  8221  ax1rid  8245  axcnre  8249  peano5nnnn  8260  peano2cn  8463  peano2re  8464  addlid  8467  subid  8547  subid1  8548  negid  8575  negeq0  8582  peano2cnm  8594  peano2rem  8595  mul01  8718  lt0neg1  8798  le0neg1  8800  recexre  8909  inelr  8915  rimul  8916  reapmul1  8926  apsqgt0  8932  mulge0  8950  negap0  8961  divvalap  9007  rerecclap  9063  div2negap  9068  divgt0i2i  9250  indconst0  9305  indconst1  9306  peano5nni  9310  nnge1  9330  times2  9436  addltmul  9547  nn0p1nn  9607  peano2nn0  9608  nn0lele2xi  9619  fcdmnn0supp  9620  fcdmnn0fsupp  9621  fcdmnn0suppg  9622  znnnlt1  9697  nn0lt10b  9731  prime  9750  msqznn  9751  zeo  9756  elnn1uz2  10017  qreccl  10052  qdivcl  10053  irrmul  10058  rphalfcl  10093  rpnegap  10098  zgt1rpn0n1  10107  ltpnf  10193  nltmnf  10201  pnfge  10202  xlt0neg1  10251  xle0neg1  10253  xaddpnf1  10259  xaddmnf1  10261  xaddid1  10275  xsubge0  10294  xleaddadd  10300  elioopnf  10380  elicopnf  10382  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  fzprval  10500  fzofzp1  10656  fzostep1  10667  flqge0nn0  10742  flqge1nn  10743  fldiv4p1lem1div2  10754  exp1  10996  qexpclz  11011  nn0sqcl  11017  expeq0  11021  expubnd  11047  sqval  11048  sqeq0  11053  resqcl  11058  zsqcl  11061  iexpcyc  11095  binom21  11103  bcnn  11210  bcn2  11217  bcn2p1  11224  bcnm1  11226  fihasheq0  11247  hashsng  11252  fihashen1  11253  fimaxq  11285  hashf1lem2  11301  iswrddm0  11343  ccatval2  11381  ccatsymb  11385  ccatrid  11390  eqs1  11411  s111  11414  swrdnd  11446  pfx00g  11462  shftfibg  11600  shftfib  11603  reim0  11641  imval2  11674  cjap0  11688  cjne0  11689  rexuz3  11771  resqrexlemover  11791  abssq  11863  nn0abscl  11867  nnabscl  11882  abs2dif  11888  max0addsup  12001  climshft  12088  bcxmas  12274  efgt1p2  12480  efgt1p  12481  efi4p  12502  resin4p  12503  recos4p  12504  sinbnd  12537  cosbnd  12538  dvdsval2  12575  zdvdsdc  12597  dvdsmul2  12599  dvdsmulcr  12606  dvdsabseq  12632  divconjdvds  12634  alzdvds  12639  fzo0dvdseq  12642  odd2np1lem  12657  mod2eq1n2dvds  12664  flodddiv4  12721  flodddiv4t2lthalf  12724  bits0  12733  bitsp1o  12738  gcdmndc  12750  gcd0id  12774  gcd1  12782  dfgcd2  12809  gcdmultiple  12815  gcdmultiplez  12816  dvdssq  12826  lcmmndc  12858  lcm0val  12861  dvdslcm  12865  lcmeq0  12867  lcmgcd  12874  lcmdvds  12875  lcmid  12876  lcm1  12877  cncongr2  12900  isprm3  12914  prm2orodd  12922  sqrt2irrap  12978  phiprm  13023  pc0  13105  pcxqcl  13113  pcdvdstr  13128  ballotfilem2  13279  ballotfilemfcc  13284  ballotfilem4  13292  unennn  13339  ennnfonelemim  13366  ctinfom  13370  ctinf  13372  enctlem  13374  elrestr  13652  tgval  13667  tgvalex  13668  xpsfrnel  13716  xpsfeq  13717  xpscf  13719  mulg1  13983  mulgnegnn  13986  ghmghmrn  14117  gsumconstcmn  14217  subrngintm  14571  subrgintm  14602  lsp0  14811  mulgrhm2  14996  zlmlemg  15014  zlmsca  15018  0opn  15159  topopn  15161  0cld  15265  ntropn  15270  ntrtop  15281  ntr0  15287  neipsm  15307  rest0  15332  xmetres  15535  metres  15536  mopnex  15658  tgioo  15707  cnlimcim  15824  cnlimc  15825  dvfre  15863  dveflem  15879  dvef  15880  efcn  15921  efap1p  15932  sin2pim  15967  cos2pim  15968  sinmpi  15969  cosmpi  15970  sinppi  15971  cosppi  15972  efimpi  15973  sincosq1lem  15979  sincosq2sgn  15981  sincosq3sgn  15982  sincosq4sgn  15983  sinq12gt0  15984  sinq34lt0t  15985  sincosq1eq  15993  abssinper  16000  logrpap0b  16031  loglt1b  16048  rpcxp0  16056  rpcxp1  16057  rpcxpsqrt  16080  logsqrt  16081  rprelogbdiv  16115  ppiqp1le  16189  ppiqeq0  16202  ppiublem1  16213  ppiqub  16215  chtqub  16218  lgs0  16254  lgs2  16258  lgsneg  16265  lgsdilem  16268  lgsdir2lem2  16270  lgsdir2lem4  16272  lgsdir2lem5  16273  lgsne0  16279  2lgslem1a2  16328  2lgslem1c  16331  upgr0eop  16485  uspgrushgr  16543  usgruspgr  16546  usgr0eop  16605  0grsubgr  16627  wlklenvclwlk  16736  upgr2wlkdc  16740  clwwlk0on0  16794  konigsbergssiedgwen  16849  bj-inf2vnlem1  17118  pwle2  17150  pwf1oexmid  17151  domomsubct  17153  nninfsellemeqinf  17181  sbthom  17193  qdiff  17220  iswomninnlem  17221  redc0  17229