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  1340  equs4  1739  sb4bor  1849  elvd  2768  eueq2dc  2937  sbcgf  3057  csbconstgf  3097  sbcnestg  3138  csbnestg  3139  csbnest1g  3140  ssindif0im  3511  mpteq1  4118  iinexgm  4188  exmid1stab  4242  mss  4260  eusv2nf  4492  eldifpw  4513  ordtriexmid  4558  onsucsssucexmid  4564  ordsucunielexmid  4568  nn0suc  4641  xpss1  4774  xpiindim  4804  reldm0  4885  elrnmpt1s  4917  resdm  4986  resid  5004  eliniseg  5040  trinxp  5064  inimasn  5088  ssrnres  5113  cnveq0  5127  coi2  5187  relrelss  5197  funcnvres  5332  funimaex  5344  fnresin1  5375  fnresin2  5376  fresin  5439  dffv3g  5557  ssimaex  5625  dmfco  5632  fvmpt  5641  fsn  5737  fsn2  5739  elabrex  5807  elabrexg  5808  f1elima  5823  2ndconst  6289  tposfun  6327  tpostpos2  6332  tfrexlem  6401  tfri3  6434  rdgruledefgg  6442  rdgss  6450  frecsuclem  6473  frecrdg  6475  oa0  6524  om0  6525  oei0  6526  oav2  6530  oa1suc  6534  nnmsucr  6555  nnm1  6592  nnm2  6593  ecelqsg  6656  ecidg  6667  xpider  6674  qsel  6680  mapdm0  6731  map0e  6754  mapsnconst  6762  ixpsnf1o  6804  map1  6880  xp1en  6891  xpcomco  6894  xpmapenlem  6919  findcard2s  6960  findcard2d  6961  findcard2sd  6962  exmidpw  6978  residfi  7015  fidcenumlemr  7030  sbthlem7  7038  eqinfti  7095  djueq1  7115  omp1eomlem  7169  endjusym  7171  eninl  7172  eninr  7173  difinfsn  7175  finomni  7215  pm54.43  7269  exmidonfinlem  7272  2onetap  7338  mulidpi  7402  nlt1pig  7425  indpi  7426  halfnqq  7494  archnqq  7501  prarloclemarch  7502  prarloclemarch2  7503  nnnq  7506  nq0a0  7541  addpinq1  7548  prarloclemlt  7577  prarloclemlo  7578  prarloclem3  7581  prarloclemcalc  7586  nqprm  7626  addnqpr1  7646  1idprl  7674  1idpru  7675  1idpr  7676  recexprlem1ssl  7717  recexprlem1ssu  7718  ltmprr  7726  0idsr  7851  1idsr  7852  00sr  7853  pn0sr  7855  negexsr  7856  recexgt0sr  7857  ltm1sr  7861  archsr  7866  prsrcl  7868  prsradd  7870  mappsrprg  7888  map2psrprg  7889  elrealeu  7913  pitonnlem1p1  7930  peano2nnnn  7937  ax1rid  7961  axcnre  7965  peano5nnnn  7976  peano2cn  8178  peano2re  8179  addlid  8182  subid  8262  subid1  8263  negid  8290  negeq0  8297  peano2cnm  8309  peano2rem  8310  mul01  8432  lt0neg1  8512  le0neg1  8514  recexre  8622  inelr  8628  rimul  8629  reapmul1  8639  apsqgt0  8645  mulge0  8663  negap0  8674  divvalap  8718  rerecclap  8774  div2negap  8779  divgt0i2i  8961  peano5nni  9010  nnge1  9030  times2  9136  addltmul  9245  nn0p1nn  9305  peano2nn0  9306  nn0lele2xi  9317  znnnlt1  9391  nn0lt10b  9423  prime  9442  msqznn  9443  zeo  9448  elnn1uz2  9698  qreccl  9733  qdivcl  9734  irrmul  9738  rphalfcl  9773  rpnegap  9778  zgt1rpn0n1  9787  ltpnf  9872  nltmnf  9880  pnfge  9881  xlt0neg1  9930  xle0neg1  9932  xaddpnf1  9938  xaddmnf1  9940  xaddid1  9954  xsubge0  9973  xleaddadd  9979  elioopnf  10059  elicopnf  10061  iccshftri  10087  iccshftli  10089  iccdili  10091  icccntri  10093  fzprval  10174  fzofzp1  10320  fzostep1  10330  flqge0nn0  10400  flqge1nn  10401  fldiv4p1lem1div2  10412  exp1  10654  qexpclz  10669  nn0sqcl  10675  expeq0  10679  expubnd  10705  sqval  10706  sqeq0  10711  resqcl  10716  zsqcl  10719  iexpcyc  10753  binom21  10761  bcnn  10866  bcn2  10873  bcn2p1  10879  bcnm1  10881  fihasheq0  10902  hashsng  10907  fihashen1  10908  fimaxq  10936  iswrddm0  10976  shftfibg  11002  shftfib  11005  reim0  11043  imval2  11076  cjap0  11089  cjne0  11090  rexuz3  11172  resqrexlemover  11192  abssq  11263  nn0abscl  11267  nnabscl  11282  abs2dif  11288  max0addsup  11401  climshft  11486  bcxmas  11671  efgt1p2  11877  efgt1p  11878  efi4p  11899  resin4p  11900  recos4p  11901  sinbnd  11934  cosbnd  11935  dvdsval2  11972  zdvdsdc  11994  dvdsmul2  11996  dvdsmulcr  12003  dvdsabseq  12029  divconjdvds  12031  alzdvds  12036  fzo0dvdseq  12039  odd2np1lem  12054  mod2eq1n2dvds  12061  flodddiv4  12118  flodddiv4t2lthalf  12121  bits0  12130  bitsp1o  12135  gcdmndc  12147  gcd0id  12171  gcd1  12179  dfgcd2  12206  gcdmultiple  12212  gcdmultiplez  12213  dvdssq  12223  lcmmndc  12255  lcm0val  12258  dvdslcm  12262  lcmeq0  12264  lcmgcd  12271  lcmdvds  12272  lcmid  12273  lcm1  12274  cncongr2  12297  isprm3  12311  prm2orodd  12319  sqrt2irrap  12373  phiprm  12416  pc0  12498  pcxqcl  12506  pcdvdstr  12521  unennn  12639  ennnfonelemim  12666  ctinfom  12670  ctinf  12672  enctlem  12674  elrestr  12949  tgval  12964  tgvalex  12965  xpsfrnel  13046  xpsfeq  13047  xpscf  13049  mulg1  13335  mulgnegnn  13338  ghmghmrn  13469  subrngintm  13844  subrgintm  13875  lsp0  14055  mulgrhm2  14242  zlmlemg  14260  zlmsca  14264  0opn  14326  topopn  14328  0cld  14432  ntropn  14437  ntrtop  14448  ntr0  14454  neipsm  14474  rest0  14499  xmetres  14702  metres  14703  mopnex  14825  tgioo  14874  cnlimcim  14991  cnlimc  14992  dvfre  15030  dveflem  15046  dvef  15047  efcn  15088  sin2pim  15133  cos2pim  15134  sinmpi  15135  cosmpi  15136  sinppi  15137  cosppi  15138  efimpi  15139  sincosq1lem  15145  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  sinq34lt0t  15151  sincosq1eq  15159  abssinper  15166  logrpap0b  15196  loglt1b  15213  rpcxp0  15218  rpcxp1  15219  rpcxpsqrt  15242  logsqrt  15243  rprelogbdiv  15277  lgs0  15338  lgs2  15342  lgsneg  15349  lgsdilem  15352  lgsdir2lem2  15354  lgsdir2lem4  15356  lgsdir2lem5  15357  lgsne0  15363  2lgslem1a2  15412  2lgslem1c  15415  bj-inf2vnlem1  15700  pwle2  15729  pwf1oexmid  15730  domomsubct  15732  nninfsellemeqinf  15747  sbthom  15757  iswomninnlem  15780  redc0  15788