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  1342  equs4  1749  sb4bor  1859  elvd  2778  eueq2dc  2948  sbcgf  3068  csbconstgf  3108  sbcnestg  3149  csbnestg  3150  csbnest1g  3151  ssindif0im  3522  mpteq1  4133  iinexgm  4203  exmid1stab  4257  mss  4275  eusv2nf  4508  eldifpw  4529  ordtriexmid  4574  onsucsssucexmid  4580  ordsucunielexmid  4584  nn0suc  4657  xpss1  4790  xpiindim  4820  reldm0  4902  elrnmpt1s  4934  resdm  5004  resid  5022  eliniseg  5058  trinxp  5082  inimasn  5106  ssrnres  5131  cnveq0  5145  coi2  5205  relrelss  5215  funcnvres  5353  funimaex  5365  fnresin1  5397  fnresin2  5398  fresin  5463  dffv3g  5582  ssimaex  5650  dmfco  5657  fvmpt  5666  fsn  5762  fsn2  5764  funop  5773  elabrex  5836  elabrexg  5837  f1elima  5852  2ndconst  6318  tposfun  6356  tpostpos2  6361  tfrexlem  6430  tfri3  6463  rdgruledefgg  6471  rdgss  6479  frecsuclem  6502  frecrdg  6504  oa0  6553  om0  6554  oei0  6555  oav2  6559  oa1suc  6563  nnmsucr  6584  nnm1  6621  nnm2  6622  ecelqsg  6685  ecidg  6696  xpider  6703  qsel  6709  mapdm0  6760  map0e  6783  mapsnconst  6791  ixpsnf1o  6833  map1  6915  xp1en  6930  xpcomco  6933  xpmapenlem  6958  findcard2s  6999  findcard2d  7000  findcard2sd  7001  exmidpw  7017  residfi  7054  fidcenumlemr  7069  sbthlem7  7077  eqinfti  7134  djueq1  7154  omp1eomlem  7208  endjusym  7210  eninl  7211  eninr  7212  difinfsn  7214  finomni  7254  pm54.43  7310  exmidonfinlem  7314  2onetap  7380  mulidpi  7444  nlt1pig  7467  indpi  7468  halfnqq  7536  archnqq  7543  prarloclemarch  7544  prarloclemarch2  7545  nnnq  7548  nq0a0  7583  addpinq1  7590  prarloclemlt  7619  prarloclemlo  7620  prarloclem3  7623  prarloclemcalc  7628  nqprm  7668  addnqpr1  7688  1idprl  7716  1idpru  7717  1idpr  7718  recexprlem1ssl  7759  recexprlem1ssu  7760  ltmprr  7768  0idsr  7893  1idsr  7894  00sr  7895  pn0sr  7897  negexsr  7898  recexgt0sr  7899  ltm1sr  7903  archsr  7908  prsrcl  7910  prsradd  7912  mappsrprg  7930  map2psrprg  7931  elrealeu  7955  pitonnlem1p1  7972  peano2nnnn  7979  ax1rid  8003  axcnre  8007  peano5nnnn  8018  peano2cn  8220  peano2re  8221  addlid  8224  subid  8304  subid1  8305  negid  8332  negeq0  8339  peano2cnm  8351  peano2rem  8352  mul01  8474  lt0neg1  8554  le0neg1  8556  recexre  8664  inelr  8670  rimul  8671  reapmul1  8681  apsqgt0  8687  mulge0  8705  negap0  8716  divvalap  8760  rerecclap  8816  div2negap  8821  divgt0i2i  9003  peano5nni  9052  nnge1  9072  times2  9178  addltmul  9287  nn0p1nn  9347  peano2nn0  9348  nn0lele2xi  9359  znnnlt1  9433  nn0lt10b  9466  prime  9485  msqznn  9486  zeo  9491  elnn1uz2  9741  qreccl  9776  qdivcl  9777  irrmul  9781  rphalfcl  9816  rpnegap  9821  zgt1rpn0n1  9830  ltpnf  9915  nltmnf  9923  pnfge  9924  xlt0neg1  9973  xle0neg1  9975  xaddpnf1  9981  xaddmnf1  9983  xaddid1  9997  xsubge0  10016  xleaddadd  10022  elioopnf  10102  elicopnf  10104  iccshftri  10130  iccshftli  10132  iccdili  10134  icccntri  10136  fzprval  10217  fzofzp1  10369  fzostep1  10379  flqge0nn0  10449  flqge1nn  10450  fldiv4p1lem1div2  10461  exp1  10703  qexpclz  10718  nn0sqcl  10724  expeq0  10728  expubnd  10754  sqval  10755  sqeq0  10760  resqcl  10765  zsqcl  10768  iexpcyc  10802  binom21  10810  bcnn  10915  bcn2  10922  bcn2p1  10928  bcnm1  10930  fihasheq0  10951  hashsng  10956  fihashen1  10957  fimaxq  10985  iswrddm0  11031  ccatval2  11068  ccatsymb  11072  ccatrid  11077  eqs1  11096  s111  11099  swrdnd  11126  pfx00g  11142  shftfibg  11181  shftfib  11184  reim0  11222  imval2  11255  cjap0  11268  cjne0  11269  rexuz3  11351  resqrexlemover  11371  abssq  11442  nn0abscl  11446  nnabscl  11461  abs2dif  11467  max0addsup  11580  climshft  11665  bcxmas  11850  efgt1p2  12056  efgt1p  12057  efi4p  12078  resin4p  12079  recos4p  12080  sinbnd  12113  cosbnd  12114  dvdsval2  12151  zdvdsdc  12173  dvdsmul2  12175  dvdsmulcr  12182  dvdsabseq  12208  divconjdvds  12210  alzdvds  12215  fzo0dvdseq  12218  odd2np1lem  12233  mod2eq1n2dvds  12240  flodddiv4  12297  flodddiv4t2lthalf  12300  bits0  12309  bitsp1o  12314  gcdmndc  12326  gcd0id  12350  gcd1  12358  dfgcd2  12385  gcdmultiple  12391  gcdmultiplez  12392  dvdssq  12402  lcmmndc  12434  lcm0val  12437  dvdslcm  12441  lcmeq0  12443  lcmgcd  12450  lcmdvds  12451  lcmid  12452  lcm1  12453  cncongr2  12476  isprm3  12490  prm2orodd  12498  sqrt2irrap  12552  phiprm  12595  pc0  12677  pcxqcl  12685  pcdvdstr  12700  unennn  12818  ennnfonelemim  12845  ctinfom  12849  ctinf  12851  enctlem  12853  elrestr  13129  tgval  13144  tgvalex  13145  xpsfrnel  13226  xpsfeq  13227  xpscf  13229  mulg1  13515  mulgnegnn  13518  ghmghmrn  13649  subrngintm  14024  subrgintm  14055  lsp0  14235  mulgrhm2  14422  zlmlemg  14440  zlmsca  14444  0opn  14528  topopn  14530  0cld  14634  ntropn  14639  ntrtop  14650  ntr0  14656  neipsm  14676  rest0  14701  xmetres  14904  metres  14905  mopnex  15027  tgioo  15076  cnlimcim  15193  cnlimc  15194  dvfre  15232  dveflem  15248  dvef  15249  efcn  15290  sin2pim  15335  cos2pim  15336  sinmpi  15337  cosmpi  15338  sinppi  15339  cosppi  15340  efimpi  15341  sincosq1lem  15347  sincosq2sgn  15349  sincosq3sgn  15350  sincosq4sgn  15351  sinq12gt0  15352  sinq34lt0t  15353  sincosq1eq  15361  abssinper  15368  logrpap0b  15398  loglt1b  15415  rpcxp0  15420  rpcxp1  15421  rpcxpsqrt  15444  logsqrt  15445  rprelogbdiv  15479  lgs0  15540  lgs2  15544  lgsneg  15551  lgsdilem  15554  lgsdir2lem2  15556  lgsdir2lem4  15558  lgsdir2lem5  15559  lgsne0  15565  2lgslem1a2  15614  2lgslem1c  15617  upgr0eop  15765  bj-inf2vnlem1  16020  dom1o  16043  pwle2  16050  pwf1oexmid  16051  domomsubct  16053  nninfsellemeqinf  16068  sbthom  16080  iswomninnlem  16103  redc0  16111