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  1366  equs4  1773  sb4bor  1884  elvd  2820  eueq2dc  2993  sbcgf  3113  csbconstgf  3154  sbcnestg  3195  csbnestg  3196  csbnest1g  3197  ssindif0im  3572  mpteq1  4199  iinexgm  4271  exmid1stab  4326  mss  4347  eusv2nf  4582  eldifpw  4603  ordtriexmid  4648  onsucsssucexmid  4654  ordsucunielexmid  4658  nn0suc  4731  xpss1  4865  xpiindim  4897  reldm0  4979  elrnmpt1s  5012  resdm  5082  resid  5100  eliniseg  5137  trinxp  5161  inimasn  5185  ssrnres  5210  cnveq0  5224  coi2  5284  relrelss  5294  funcnvres  5434  funimaex  5446  fnresin1  5478  fnresin2  5479  fresin  5548  dffv3g  5671  ssimaex  5743  dmfco  5750  fvmpt  5759  fsn  5854  fsn2  5856  funop  5866  elabrex  5936  elabrexg  5937  f1elima  5952  2ndconst  6431  tposfun  6504  tpostpos2  6509  tfrexlem  6578  tfri3  6611  rdgruledefgg  6619  rdgss  6627  frecsuclem  6650  frecrdg  6652  oa0  6703  om0  6704  oei0  6705  oav2  6709  oa1suc  6713  nnmsucr  6734  nnm1  6771  nnm2  6772  ecelqsg  6835  ecidg  6846  xpider  6853  qsel  6859  mapdm0  6910  map0e  6933  mapsnconst  6942  ixpsnf1o  6984  map1  7067  dom1o  7082  xp1en  7087  xpcomco  7090  xpmapenlem  7115  findcard2s  7160  findcard2d  7161  findcard2sd  7162  exmidpw  7181  residfi  7220  fidcenumlemr  7238  sbthlem7  7246  eqinfti  7324  djueq1  7344  omp1eomlem  7398  endjusym  7400  eninl  7401  eninr  7402  difinfsn  7404  finomni  7444  pm54.43  7500  exmidonfinlem  7509  2onetap  7585  mulidpi  7649  nlt1pig  7672  indpi  7673  halfnqq  7741  archnqq  7748  prarloclemarch  7749  prarloclemarch2  7750  nnnq  7753  nq0a0  7788  addpinq1  7795  prarloclemlt  7824  prarloclemlo  7825  prarloclem3  7828  prarloclemcalc  7833  nqprm  7873  addnqpr1  7893  1idprl  7921  1idpru  7922  1idpr  7923  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  0idsr  8098  1idsr  8099  00sr  8100  pn0sr  8102  negexsr  8103  recexgt0sr  8104  ltm1sr  8108  archsr  8113  prsrcl  8115  prsradd  8117  mappsrprg  8135  map2psrprg  8136  elrealeu  8160  pitonnlem1p1  8177  peano2nnnn  8184  ax1rid  8208  axcnre  8212  peano5nnnn  8223  peano2cn  8425  peano2re  8426  addlid  8429  subid  8509  subid1  8510  negid  8537  negeq0  8544  peano2cnm  8556  peano2rem  8557  mul01  8680  lt0neg1  8760  le0neg1  8762  recexre  8870  inelr  8876  rimul  8877  reapmul1  8887  apsqgt0  8893  mulge0  8911  negap0  8922  divvalap  8968  rerecclap  9024  div2negap  9029  divgt0i2i  9211  peano5nni  9260  nnge1  9280  times2  9386  addltmul  9495  nn0p1nn  9555  peano2nn0  9556  nn0lele2xi  9567  fcdmnn0supp  9568  fcdmnn0fsupp  9569  fcdmnn0suppg  9570  znnnlt1  9645  nn0lt10b  9679  prime  9698  msqznn  9699  zeo  9704  elnn1uz2  9960  qreccl  9995  qdivcl  9996  irrmul  10000  rphalfcl  10035  rpnegap  10040  zgt1rpn0n1  10049  ltpnf  10135  nltmnf  10143  pnfge  10144  xlt0neg1  10193  xle0neg1  10195  xaddpnf1  10201  xaddmnf1  10203  xaddid1  10217  xsubge0  10236  xleaddadd  10242  elioopnf  10322  elicopnf  10324  iccshftri  10350  iccshftli  10352  iccdili  10354  icccntri  10356  fzprval  10441  fzofzp1  10597  fzostep1  10608  flqge0nn0  10680  flqge1nn  10681  fldiv4p1lem1div2  10692  exp1  10934  qexpclz  10949  nn0sqcl  10955  expeq0  10959  expubnd  10985  sqval  10986  sqeq0  10991  resqcl  10996  zsqcl  10999  iexpcyc  11033  binom21  11041  bcnn  11147  bcn2  11154  bcn2p1  11161  bcnm1  11163  fihasheq0  11184  hashsng  11189  fihashen1  11190  fimaxq  11222  iswrddm0  11276  ccatval2  11314  ccatsymb  11318  ccatrid  11323  eqs1  11344  s111  11347  swrdnd  11379  pfx00g  11395  shftfibg  11533  shftfib  11536  reim0  11574  imval2  11607  cjap0  11621  cjne0  11622  rexuz3  11704  resqrexlemover  11724  abssq  11795  nn0abscl  11799  nnabscl  11814  abs2dif  11820  max0addsup  11933  climshft  12018  bcxmas  12204  efgt1p2  12410  efgt1p  12411  efi4p  12432  resin4p  12433  recos4p  12434  sinbnd  12467  cosbnd  12468  dvdsval2  12505  zdvdsdc  12527  dvdsmul2  12529  dvdsmulcr  12536  dvdsabseq  12562  divconjdvds  12564  alzdvds  12569  fzo0dvdseq  12572  odd2np1lem  12587  mod2eq1n2dvds  12594  flodddiv4  12651  flodddiv4t2lthalf  12654  bits0  12663  bitsp1o  12668  gcdmndc  12680  gcd0id  12704  gcd1  12712  dfgcd2  12739  gcdmultiple  12745  gcdmultiplez  12746  dvdssq  12756  lcmmndc  12788  lcm0val  12791  dvdslcm  12795  lcmeq0  12797  lcmgcd  12804  lcmdvds  12805  lcmid  12806  lcm1  12807  cncongr2  12830  isprm3  12844  prm2orodd  12852  sqrt2irrap  12906  phiprm  12949  pc0  13031  pcxqcl  13039  pcdvdstr  13054  ballotfilem2  13176  ballotfilemfcc  13181  ballotfilem4  13189  unennn  13236  ennnfonelemim  13263  ctinfom  13267  ctinf  13269  enctlem  13271  elrestr  13548  tgval  13563  tgvalex  13564  xpsfrnel  13612  xpsfeq  13613  xpscf  13615  mulg1  13886  mulgnegnn  13889  ghmghmrn  14020  subrngintm  14462  subrgintm  14493  lsp0  14701  mulgrhm2  14888  zlmlemg  14906  zlmsca  14910  0opn  15001  topopn  15003  0cld  15107  ntropn  15112  ntrtop  15123  ntr0  15129  neipsm  15149  rest0  15174  xmetres  15377  metres  15378  mopnex  15500  tgioo  15549  cnlimcim  15666  cnlimc  15667  dvfre  15705  dveflem  15721  dvef  15722  efcn  15763  sin2pim  15808  cos2pim  15809  sinmpi  15810  cosmpi  15811  sinppi  15812  cosppi  15813  efimpi  15814  sincosq1lem  15820  sincosq2sgn  15822  sincosq3sgn  15823  sincosq4sgn  15824  sinq12gt0  15825  sinq34lt0t  15826  sincosq1eq  15834  abssinper  15841  logrpap0b  15871  loglt1b  15888  rpcxp0  15893  rpcxp1  15894  rpcxpsqrt  15917  logsqrt  15918  rprelogbdiv  15952  lgs0  16016  lgs2  16020  lgsneg  16027  lgsdilem  16030  lgsdir2lem2  16032  lgsdir2lem4  16034  lgsdir2lem5  16035  lgsne0  16041  2lgslem1a2  16090  2lgslem1c  16093  upgr0eop  16247  uspgrushgr  16305  usgruspgr  16308  usgr0eop  16367  0grsubgr  16389  wlklenvclwlk  16498  upgr2wlkdc  16502  clwwlk0on0  16556  konigsbergssiedgwen  16611  bj-inf2vnlem1  16880  pwle2  16912  pwf1oexmid  16913  domomsubct  16915  nninfsellemeqinf  16934  sbthom  16946  qdiff  16973  iswomninnlem  16974  redc0  16982