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  7271  exmidonfinlem  7274  2onetap  7340  mulidpi  7404  nlt1pig  7427  indpi  7428  halfnqq  7496  archnqq  7503  prarloclemarch  7504  prarloclemarch2  7505  nnnq  7508  nq0a0  7543  addpinq1  7550  prarloclemlt  7579  prarloclemlo  7580  prarloclem3  7583  prarloclemcalc  7588  nqprm  7628  addnqpr1  7648  1idprl  7676  1idpru  7677  1idpr  7678  recexprlem1ssl  7719  recexprlem1ssu  7720  ltmprr  7728  0idsr  7853  1idsr  7854  00sr  7855  pn0sr  7857  negexsr  7858  recexgt0sr  7859  ltm1sr  7863  archsr  7868  prsrcl  7870  prsradd  7872  mappsrprg  7890  map2psrprg  7891  elrealeu  7915  pitonnlem1p1  7932  peano2nnnn  7939  ax1rid  7963  axcnre  7967  peano5nnnn  7978  peano2cn  8180  peano2re  8181  addlid  8184  subid  8264  subid1  8265  negid  8292  negeq0  8299  peano2cnm  8311  peano2rem  8312  mul01  8434  lt0neg1  8514  le0neg1  8516  recexre  8624  inelr  8630  rimul  8631  reapmul1  8641  apsqgt0  8647  mulge0  8665  negap0  8676  divvalap  8720  rerecclap  8776  div2negap  8781  divgt0i2i  8963  peano5nni  9012  nnge1  9032  times2  9138  addltmul  9247  nn0p1nn  9307  peano2nn0  9308  nn0lele2xi  9319  znnnlt1  9393  nn0lt10b  9425  prime  9444  msqznn  9445  zeo  9450  elnn1uz2  9700  qreccl  9735  qdivcl  9736  irrmul  9740  rphalfcl  9775  rpnegap  9780  zgt1rpn0n1  9789  ltpnf  9874  nltmnf  9882  pnfge  9883  xlt0neg1  9932  xle0neg1  9934  xaddpnf1  9940  xaddmnf1  9942  xaddid1  9956  xsubge0  9975  xleaddadd  9981  elioopnf  10061  elicopnf  10063  iccshftri  10089  iccshftli  10091  iccdili  10093  icccntri  10095  fzprval  10176  fzofzp1  10322  fzostep1  10332  flqge0nn0  10402  flqge1nn  10403  fldiv4p1lem1div2  10414  exp1  10656  qexpclz  10671  nn0sqcl  10677  expeq0  10681  expubnd  10707  sqval  10708  sqeq0  10713  resqcl  10718  zsqcl  10721  iexpcyc  10755  binom21  10763  bcnn  10868  bcn2  10875  bcn2p1  10881  bcnm1  10883  fihasheq0  10904  hashsng  10909  fihashen1  10910  fimaxq  10938  iswrddm0  10978  shftfibg  11004  shftfib  11007  reim0  11045  imval2  11078  cjap0  11091  cjne0  11092  rexuz3  11174  resqrexlemover  11194  abssq  11265  nn0abscl  11269  nnabscl  11284  abs2dif  11290  max0addsup  11403  climshft  11488  bcxmas  11673  efgt1p2  11879  efgt1p  11880  efi4p  11901  resin4p  11902  recos4p  11903  sinbnd  11936  cosbnd  11937  dvdsval2  11974  zdvdsdc  11996  dvdsmul2  11998  dvdsmulcr  12005  dvdsabseq  12031  divconjdvds  12033  alzdvds  12038  fzo0dvdseq  12041  odd2np1lem  12056  mod2eq1n2dvds  12063  flodddiv4  12120  flodddiv4t2lthalf  12123  bits0  12132  bitsp1o  12137  gcdmndc  12149  gcd0id  12173  gcd1  12181  dfgcd2  12208  gcdmultiple  12214  gcdmultiplez  12215  dvdssq  12225  lcmmndc  12257  lcm0val  12260  dvdslcm  12264  lcmeq0  12266  lcmgcd  12273  lcmdvds  12274  lcmid  12275  lcm1  12276  cncongr2  12299  isprm3  12313  prm2orodd  12321  sqrt2irrap  12375  phiprm  12418  pc0  12500  pcxqcl  12508  pcdvdstr  12523  unennn  12641  ennnfonelemim  12668  ctinfom  12672  ctinf  12674  enctlem  12676  elrestr  12951  tgval  12966  tgvalex  12967  xpsfrnel  13048  xpsfeq  13049  xpscf  13051  mulg1  13337  mulgnegnn  13340  ghmghmrn  13471  subrngintm  13846  subrgintm  13877  lsp0  14057  mulgrhm2  14244  zlmlemg  14262  zlmsca  14266  0opn  14350  topopn  14352  0cld  14456  ntropn  14461  ntrtop  14472  ntr0  14478  neipsm  14498  rest0  14523  xmetres  14726  metres  14727  mopnex  14849  tgioo  14898  cnlimcim  15015  cnlimc  15016  dvfre  15054  dveflem  15070  dvef  15071  efcn  15112  sin2pim  15157  cos2pim  15158  sinmpi  15159  cosmpi  15160  sinppi  15161  cosppi  15162  efimpi  15163  sincosq1lem  15169  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  sinq34lt0t  15175  sincosq1eq  15183  abssinper  15190  logrpap0b  15220  loglt1b  15237  rpcxp0  15242  rpcxp1  15243  rpcxpsqrt  15266  logsqrt  15267  rprelogbdiv  15301  lgs0  15362  lgs2  15366  lgsneg  15373  lgsdilem  15376  lgsdir2lem2  15378  lgsdir2lem4  15380  lgsdir2lem5  15381  lgsne0  15387  2lgslem1a2  15436  2lgslem1c  15439  bj-inf2vnlem1  15724  pwle2  15753  pwf1oexmid  15754  domomsubct  15756  nninfsellemeqinf  15771  sbthom  15783  iswomninnlem  15806  redc0  15814