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  1363  equs4  1771  sb4bor  1881  elvd  2804  eueq2dc  2976  sbcgf  3096  csbconstgf  3137  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  ssindif0im  3551  mpteq1  4167  iinexgm  4237  exmid1stab  4291  mss  4311  eusv2nf  4544  eldifpw  4565  ordtriexmid  4610  onsucsssucexmid  4616  ordsucunielexmid  4620  nn0suc  4693  xpss1  4826  xpiindim  4856  reldm0  4938  elrnmpt1s  4970  resdm  5040  resid  5058  eliniseg  5094  trinxp  5118  inimasn  5142  ssrnres  5167  cnveq0  5181  coi2  5241  relrelss  5251  funcnvres  5390  funimaex  5402  fnresin1  5434  fnresin2  5435  fresin  5500  dffv3g  5619  ssimaex  5688  dmfco  5695  fvmpt  5704  fsn  5800  fsn2  5802  funop  5811  elabrex  5874  elabrexg  5875  f1elima  5890  2ndconst  6358  tposfun  6396  tpostpos2  6401  tfrexlem  6470  tfri3  6503  rdgruledefgg  6511  rdgss  6519  frecsuclem  6542  frecrdg  6544  oa0  6593  om0  6594  oei0  6595  oav2  6599  oa1suc  6603  nnmsucr  6624  nnm1  6661  nnm2  6662  ecelqsg  6725  ecidg  6736  xpider  6743  qsel  6749  mapdm0  6800  map0e  6823  mapsnconst  6831  ixpsnf1o  6873  map1  6955  xp1en  6970  xpcomco  6973  xpmapenlem  6998  findcard2s  7040  findcard2d  7041  findcard2sd  7042  exmidpw  7058  residfi  7095  fidcenumlemr  7110  sbthlem7  7118  eqinfti  7175  djueq1  7195  omp1eomlem  7249  endjusym  7251  eninl  7252  eninr  7253  difinfsn  7255  finomni  7295  pm54.43  7351  exmidonfinlem  7359  2onetap  7429  mulidpi  7493  nlt1pig  7516  indpi  7517  halfnqq  7585  archnqq  7592  prarloclemarch  7593  prarloclemarch2  7594  nnnq  7597  nq0a0  7632  addpinq1  7639  prarloclemlt  7668  prarloclemlo  7669  prarloclem3  7672  prarloclemcalc  7677  nqprm  7717  addnqpr1  7737  1idprl  7765  1idpru  7766  1idpr  7767  recexprlem1ssl  7808  recexprlem1ssu  7809  ltmprr  7817  0idsr  7942  1idsr  7943  00sr  7944  pn0sr  7946  negexsr  7947  recexgt0sr  7948  ltm1sr  7952  archsr  7957  prsrcl  7959  prsradd  7961  mappsrprg  7979  map2psrprg  7980  elrealeu  8004  pitonnlem1p1  8021  peano2nnnn  8028  ax1rid  8052  axcnre  8056  peano5nnnn  8067  peano2cn  8269  peano2re  8270  addlid  8273  subid  8353  subid1  8354  negid  8381  negeq0  8388  peano2cnm  8400  peano2rem  8401  mul01  8523  lt0neg1  8603  le0neg1  8605  recexre  8713  inelr  8719  rimul  8720  reapmul1  8730  apsqgt0  8736  mulge0  8754  negap0  8765  divvalap  8809  rerecclap  8865  div2negap  8870  divgt0i2i  9052  peano5nni  9101  nnge1  9121  times2  9227  addltmul  9336  nn0p1nn  9396  peano2nn0  9397  nn0lele2xi  9408  znnnlt1  9482  nn0lt10b  9515  prime  9534  msqznn  9535  zeo  9540  elnn1uz2  9790  qreccl  9825  qdivcl  9826  irrmul  9830  rphalfcl  9865  rpnegap  9870  zgt1rpn0n1  9879  ltpnf  9964  nltmnf  9972  pnfge  9973  xlt0neg1  10022  xle0neg1  10024  xaddpnf1  10030  xaddmnf1  10032  xaddid1  10046  xsubge0  10065  xleaddadd  10071  elioopnf  10151  elicopnf  10153  iccshftri  10179  iccshftli  10181  iccdili  10183  icccntri  10185  fzprval  10266  fzofzp1  10420  fzostep1  10430  flqge0nn0  10500  flqge1nn  10501  fldiv4p1lem1div2  10512  exp1  10754  qexpclz  10769  nn0sqcl  10775  expeq0  10779  expubnd  10805  sqval  10806  sqeq0  10811  resqcl  10816  zsqcl  10819  iexpcyc  10853  binom21  10861  bcnn  10966  bcn2  10973  bcn2p1  10979  bcnm1  10981  fihasheq0  11002  hashsng  11007  fihashen1  11008  fimaxq  11036  iswrddm0  11082  ccatval2  11119  ccatsymb  11123  ccatrid  11128  eqs1  11147  s111  11150  swrdnd  11177  pfx00g  11193  shftfibg  11317  shftfib  11320  reim0  11358  imval2  11391  cjap0  11404  cjne0  11405  rexuz3  11487  resqrexlemover  11507  abssq  11578  nn0abscl  11582  nnabscl  11597  abs2dif  11603  max0addsup  11716  climshft  11801  bcxmas  11986  efgt1p2  12192  efgt1p  12193  efi4p  12214  resin4p  12215  recos4p  12216  sinbnd  12249  cosbnd  12250  dvdsval2  12287  zdvdsdc  12309  dvdsmul2  12311  dvdsmulcr  12318  dvdsabseq  12344  divconjdvds  12346  alzdvds  12351  fzo0dvdseq  12354  odd2np1lem  12369  mod2eq1n2dvds  12376  flodddiv4  12433  flodddiv4t2lthalf  12436  bits0  12445  bitsp1o  12450  gcdmndc  12462  gcd0id  12486  gcd1  12494  dfgcd2  12521  gcdmultiple  12527  gcdmultiplez  12528  dvdssq  12538  lcmmndc  12570  lcm0val  12573  dvdslcm  12577  lcmeq0  12579  lcmgcd  12586  lcmdvds  12587  lcmid  12588  lcm1  12589  cncongr2  12612  isprm3  12626  prm2orodd  12634  sqrt2irrap  12688  phiprm  12731  pc0  12813  pcxqcl  12821  pcdvdstr  12836  unennn  12954  ennnfonelemim  12981  ctinfom  12985  ctinf  12987  enctlem  12989  elrestr  13266  tgval  13281  tgvalex  13282  xpsfrnel  13363  xpsfeq  13364  xpscf  13366  mulg1  13652  mulgnegnn  13655  ghmghmrn  13786  subrngintm  14161  subrgintm  14192  lsp0  14372  mulgrhm2  14559  zlmlemg  14577  zlmsca  14581  0opn  14665  topopn  14667  0cld  14771  ntropn  14776  ntrtop  14787  ntr0  14793  neipsm  14813  rest0  14838  xmetres  15041  metres  15042  mopnex  15164  tgioo  15213  cnlimcim  15330  cnlimc  15331  dvfre  15369  dveflem  15385  dvef  15386  efcn  15427  sin2pim  15472  cos2pim  15473  sinmpi  15474  cosmpi  15475  sinppi  15476  cosppi  15477  efimpi  15478  sincosq1lem  15484  sincosq2sgn  15486  sincosq3sgn  15487  sincosq4sgn  15488  sinq12gt0  15489  sinq34lt0t  15490  sincosq1eq  15498  abssinper  15505  logrpap0b  15535  loglt1b  15552  rpcxp0  15557  rpcxp1  15558  rpcxpsqrt  15581  logsqrt  15582  rprelogbdiv  15616  lgs0  15677  lgs2  15681  lgsneg  15688  lgsdilem  15691  lgsdir2lem2  15693  lgsdir2lem4  15695  lgsdir2lem5  15696  lgsne0  15702  2lgslem1a2  15751  2lgslem1c  15754  upgr0eop  15907  uspgrushgr  15963  usgruspgr  15966  bj-inf2vnlem1  16263  dom1o  16286  pwle2  16295  pwf1oexmid  16296  domomsubct  16298  nninfsellemeqinf  16313  sbthom  16325  iswomninnlem  16348  redc0  16356