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  1365  equs4  1773  sb4bor  1883  elvd  2807  eueq2dc  2979  sbcgf  3099  csbconstgf  3140  sbcnestg  3181  csbnestg  3182  csbnest1g  3183  ssindif0im  3554  mpteq1  4173  iinexgm  4244  exmid1stab  4298  mss  4318  eusv2nf  4553  eldifpw  4574  ordtriexmid  4619  onsucsssucexmid  4625  ordsucunielexmid  4629  nn0suc  4702  xpss1  4836  xpiindim  4867  reldm0  4949  elrnmpt1s  4982  resdm  5052  resid  5070  eliniseg  5106  trinxp  5130  inimasn  5154  ssrnres  5179  cnveq0  5193  coi2  5253  relrelss  5263  funcnvres  5403  funimaex  5415  fnresin1  5447  fnresin2  5448  fresin  5515  dffv3g  5635  ssimaex  5707  dmfco  5714  fvmpt  5723  fsn  5819  fsn2  5821  funop  5831  elabrex  5898  elabrexg  5899  f1elima  5914  2ndconst  6387  tposfun  6426  tpostpos2  6431  tfrexlem  6500  tfri3  6533  rdgruledefgg  6541  rdgss  6549  frecsuclem  6572  frecrdg  6574  oa0  6625  om0  6626  oei0  6627  oav2  6631  oa1suc  6635  nnmsucr  6656  nnm1  6693  nnm2  6694  ecelqsg  6757  ecidg  6768  xpider  6775  qsel  6781  mapdm0  6832  map0e  6855  mapsnconst  6863  ixpsnf1o  6905  map1  6987  dom1o  7002  xp1en  7007  xpcomco  7010  xpmapenlem  7035  findcard2s  7079  findcard2d  7080  findcard2sd  7081  exmidpw  7100  residfi  7139  fidcenumlemr  7154  sbthlem7  7162  eqinfti  7219  djueq1  7239  omp1eomlem  7293  endjusym  7295  eninl  7296  eninr  7297  difinfsn  7299  finomni  7339  pm54.43  7395  exmidonfinlem  7404  2onetap  7474  mulidpi  7538  nlt1pig  7561  indpi  7562  halfnqq  7630  archnqq  7637  prarloclemarch  7638  prarloclemarch2  7639  nnnq  7642  nq0a0  7677  addpinq1  7684  prarloclemlt  7713  prarloclemlo  7714  prarloclem3  7717  prarloclemcalc  7722  nqprm  7762  addnqpr1  7782  1idprl  7810  1idpru  7811  1idpr  7812  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  0idsr  7987  1idsr  7988  00sr  7989  pn0sr  7991  negexsr  7992  recexgt0sr  7993  ltm1sr  7997  archsr  8002  prsrcl  8004  prsradd  8006  mappsrprg  8024  map2psrprg  8025  elrealeu  8049  pitonnlem1p1  8066  peano2nnnn  8073  ax1rid  8097  axcnre  8101  peano5nnnn  8112  peano2cn  8314  peano2re  8315  addlid  8318  subid  8398  subid1  8399  negid  8426  negeq0  8433  peano2cnm  8445  peano2rem  8446  mul01  8568  lt0neg1  8648  le0neg1  8650  recexre  8758  inelr  8764  rimul  8765  reapmul1  8775  apsqgt0  8781  mulge0  8799  negap0  8810  divvalap  8854  rerecclap  8910  div2negap  8915  divgt0i2i  9097  peano5nni  9146  nnge1  9166  times2  9272  addltmul  9381  nn0p1nn  9441  peano2nn0  9442  nn0lele2xi  9453  znnnlt1  9527  nn0lt10b  9560  prime  9579  msqznn  9580  zeo  9585  elnn1uz2  9841  qreccl  9876  qdivcl  9877  irrmul  9881  rphalfcl  9916  rpnegap  9921  zgt1rpn0n1  9930  ltpnf  10015  nltmnf  10023  pnfge  10024  xlt0neg1  10073  xle0neg1  10075  xaddpnf1  10081  xaddmnf1  10083  xaddid1  10097  xsubge0  10116  xleaddadd  10122  elioopnf  10202  elicopnf  10204  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  fzprval  10317  fzofzp1  10473  fzostep1  10484  flqge0nn0  10554  flqge1nn  10555  fldiv4p1lem1div2  10566  exp1  10808  qexpclz  10823  nn0sqcl  10829  expeq0  10833  expubnd  10859  sqval  10860  sqeq0  10865  resqcl  10870  zsqcl  10873  iexpcyc  10907  binom21  10915  bcnn  11020  bcn2  11027  bcn2p1  11033  bcnm1  11035  fihasheq0  11056  hashsng  11061  fihashen1  11062  fimaxq  11092  iswrddm0  11141  ccatval2  11179  ccatsymb  11183  ccatrid  11188  eqs1  11209  s111  11212  swrdnd  11244  pfx00g  11260  shftfibg  11385  shftfib  11388  reim0  11426  imval2  11459  cjap0  11472  cjne0  11473  rexuz3  11555  resqrexlemover  11575  abssq  11646  nn0abscl  11650  nnabscl  11665  abs2dif  11671  max0addsup  11784  climshft  11869  bcxmas  12055  efgt1p2  12261  efgt1p  12262  efi4p  12283  resin4p  12284  recos4p  12285  sinbnd  12318  cosbnd  12319  dvdsval2  12356  zdvdsdc  12378  dvdsmul2  12380  dvdsmulcr  12387  dvdsabseq  12413  divconjdvds  12415  alzdvds  12420  fzo0dvdseq  12423  odd2np1lem  12438  mod2eq1n2dvds  12445  flodddiv4  12502  flodddiv4t2lthalf  12505  bits0  12514  bitsp1o  12519  gcdmndc  12531  gcd0id  12555  gcd1  12563  dfgcd2  12590  gcdmultiple  12596  gcdmultiplez  12597  dvdssq  12607  lcmmndc  12639  lcm0val  12642  dvdslcm  12646  lcmeq0  12648  lcmgcd  12655  lcmdvds  12656  lcmid  12657  lcm1  12658  cncongr2  12681  isprm3  12695  prm2orodd  12703  sqrt2irrap  12757  phiprm  12800  pc0  12882  pcxqcl  12890  pcdvdstr  12905  unennn  13023  ennnfonelemim  13050  ctinfom  13054  ctinf  13056  enctlem  13058  elrestr  13335  tgval  13350  tgvalex  13351  xpsfrnel  13432  xpsfeq  13433  xpscf  13435  mulg1  13721  mulgnegnn  13724  ghmghmrn  13855  subrngintm  14232  subrgintm  14263  lsp0  14443  mulgrhm2  14630  zlmlemg  14648  zlmsca  14652  0opn  14736  topopn  14738  0cld  14842  ntropn  14847  ntrtop  14858  ntr0  14864  neipsm  14884  rest0  14909  xmetres  15112  metres  15113  mopnex  15235  tgioo  15284  cnlimcim  15401  cnlimc  15402  dvfre  15440  dveflem  15456  dvef  15457  efcn  15498  sin2pim  15543  cos2pim  15544  sinmpi  15545  cosmpi  15546  sinppi  15547  cosppi  15548  efimpi  15549  sincosq1lem  15555  sincosq2sgn  15557  sincosq3sgn  15558  sincosq4sgn  15559  sinq12gt0  15560  sinq34lt0t  15561  sincosq1eq  15569  abssinper  15576  logrpap0b  15606  loglt1b  15623  rpcxp0  15628  rpcxp1  15629  rpcxpsqrt  15652  logsqrt  15653  rprelogbdiv  15687  lgs0  15748  lgs2  15752  lgsneg  15759  lgsdilem  15762  lgsdir2lem2  15764  lgsdir2lem4  15766  lgsdir2lem5  15767  lgsne0  15773  2lgslem1a2  15822  2lgslem1c  15825  upgr0eop  15979  uspgrushgr  16037  usgruspgr  16040  usgr0eop  16099  0grsubgr  16121  wlklenvclwlk  16230  upgr2wlkdc  16234  clwwlk0on0  16288  bj-inf2vnlem1  16591  pwle2  16625  pwf1oexmid  16626  domomsubct  16628  nninfsellemeqinf  16644  sbthom  16656  iswomninnlem  16679  redc0  16687