Theorem mpan2 429

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 425	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpanr12  443  mp3an23  1370  equs4  1777  sb4bor  1888  elvd  2826  eueq2dc  2999  sbcgf  3119  csbconstgf  3160  sbcnestg  3201  csbnestg  3202  csbnest1g  3203  ssindif0im  3584  mpteq1  4216  iinexgm  4292  exmid1stab  4347  mss  4368  eusv2nf  4604  eldifpw  4625  ordtriexmid  4670  onsucsssucexmid  4676  ordsucunielexmid  4680  nn0suc  4753  xpss1  4887  xpiindim  4919  reldm0  5001  elrnmpt1s  5034  resdm  5104  resid  5123  eliniseg  5160  trinxp  5184  inimasn  5208  ssrnres  5233  cnveq0  5247  coi2  5307  relrelss  5317  funcnvres  5457  funimaex  5469  fnresin1  5501  fnresin2  5502  fresin  5571  dffv3g  5694  ssimaex  5767  dmfco  5776  fvmpt  5785  fsn  5883  fsn2  5885  funop  5895  elabrex  5966  elabrexg  5967  f1elima  5982  2ndconst  6462  tposfun  6536  tpostpos2  6541  tfrexlem  6610  tfri3  6643  rdgruledefgg  6651  rdgss  6659  frecsuclem  6682  frecrdg  6684  oa0  6735  om0  6736  oei0  6737  oav2  6741  oa1suc  6745  nnmsucr  6766  nnm1  6803  nnm2  6804  ecelqsg  6867  ecidg  6878  xpider  6885  qsel  6891  mapdm0  6942  map0e  6972  mapsnconst  6982  ixpsnf1o  7024  map1  7107  dom1o  7122  xp1en  7127  xpcomco  7130  xpmapenlem  7155  findcard2s  7200  findcard2d  7201  findcard2sd  7202  exmidpw  7221  residfi  7260  fidcenumlemr  7279  sbthlem7  7287  eqinfti  7367  djueq1  7387  omp1eomlem  7441  endjusym  7443  eninl  7444  eninr  7445  difinfsn  7447  finomni  7487  pm54.43  7543  exmidonfinlem  7552  2onetap  7628  mulidpi  7692  nlt1pig  7715  indpi  7716  halfnqq  7784  archnqq  7791  prarloclemarch  7792  prarloclemarch2  7793  nnnq  7796  nq0a0  7831  addpinq1  7838  prarloclemlt  7867  prarloclemlo  7868  prarloclem3  7871  prarloclemcalc  7876  nqprm  7916  addnqpr1  7936  1idprl  7964  1idpru  7965  1idpr  7966  recexprlem1ssl  8007  recexprlem1ssu  8008  ltmprr  8016  0idsr  8141  1idsr  8142  00sr  8143  pn0sr  8145  negexsr  8146  recexgt0sr  8147  ltm1sr  8151  archsr  8156  prsrcl  8158  prsradd  8160  mappsrprg  8178  map2psrprg  8179  elrealeu  8203  pitonnlem1p1  8220  peano2nnnn  8227  ax1rid  8251  axcnre  8255  peano5nnnn  8266  peano2cn  8469  peano2re  8470  addlid  8473  subid  8553  subid1  8554  negid  8581  negeq0  8588  peano2cnm  8600  peano2rem  8601  mul01  8724  lt0neg1  8804  le0neg1  8806  recexre  8915  inelr  8921  rimul  8922  reapmul1  8932  apsqgt0  8938  mulge0  8956  negap0  8967  divvalap  9013  rerecclap  9069  div2negap  9074  divgt0i2i  9256  indconst0  9312  indconst1  9313  peano5nni  9317  nnge1  9337  times2  9443  addltmul  9554  nn0p1nn  9614  peano2nn0  9615  nn0lele2xi  9626  fcdmnn0supp  9627  fcdmnn0suppg  9628  znnnlt1  9702  nn0lt10b  9736  prime  9756  msqznn  9757  zeo  9762  elnn1uz2  10023  qreccl  10058  qdivcl  10059  irrmul  10064  rphalfcl  10099  rpnegap  10104  zgt1rpn0n1  10113  ltpnf  10199  nltmnf  10207  pnfge  10208  xlt0neg1  10257  xle0neg1  10259  xaddpnf1  10265  xaddmnf1  10267  xaddid1  10281  xsubge0  10300  xleaddadd  10306  elioopnf  10386  elicopnf  10388  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  fzprval  10506  fzofzp1  10662  fzostep1  10673  flqge0nn0  10749  flqge1nn  10750  fldiv4p1lem1div2  10761  exp1  11003  qexpclz  11018  nn0sqcl  11024  expeq0  11028  expubnd  11054  sqval  11055  sqeq0  11060  resqcl  11065  zsqcl  11068  iexpcyc  11102  binom21  11110  bcnn  11217  bcn2  11224  bcn2p1  11231  bcnm1  11233  fihasheq0  11254  hashsng  11259  fihashen1  11260  fimaxq  11292  hashf1lem2  11308  iswrddm0  11350  ccatval2  11388  ccatsymb  11392  ccatrid  11397  eqs1  11418  s111  11421  swrdnd  11453  pfx00g  11469  shftfibg  11607  shftfib  11610  reim0  11648  imval2  11681  cjap0  11695  cjne0  11696  rexuz3  11778  resqrexlemover  11798  abssq  11870  nn0abscl  11874  nnabscl  11889  abs2dif  11895  max0addsup  12008  climshft  12095  bcxmas  12281  efgt1p2  12487  efgt1p  12488  efi4p  12509  resin4p  12510  recos4p  12511  sinbnd  12544  cosbnd  12545  dvdsval2  12582  zdvdsdc  12604  dvdsmul2  12606  dvdsmulcr  12613  dvdsabseq  12639  divconjdvds  12641  alzdvds  12646  fzo0dvdseq  12649  odd2np1lem  12664  mod2eq1n2dvds  12671  flodddiv4  12728  flodddiv4t2lthalf  12731  bits0  12740  bitsp1o  12745  gcdmndc  12757  gcd0id  12781  gcd1  12789  dfgcd2  12816  gcdmultiple  12822  gcdmultiplez  12823  dvdssq  12833  lcmmndc  12865  lcm0val  12868  dvdslcm  12872  lcmeq0  12874  lcmgcd  12881  lcmdvds  12882  lcmid  12883  lcm1  12884  cncongr2  12907  isprm3  12921  prm2orodd  12929  sqrt2irrap  12985  phiprm  13030  pc0  13112  pcxqcl  13120  pcdvdstr  13135  ballotfilem2  13286  ballotfilemfcc  13291  ballotfilem4  13299  unennn  13346  ennnfonelemim  13373  ctinfom  13377  ctinf  13379  enctlem  13381  elrestr  13660  tgval  13675  tgvalex  13676  xpsfrnel  13724  xpsfeq  13725  xpscf  13727  mulg1  13991  mulgnegnn  13994  ghmghmrn  14125  cntrnsg  14176  gsumconstcmn  14266  subrngintm  14629  subrgintm  14660  lsp0  14869  mulgrhm2  15054  zlmlemg  15072  zlmsca  15076  0opn  15265  topopn  15267  0cld  15371  ntropn  15376  ntrtop  15387  ntr0  15393  neipsm  15413  rest0  15438  xmetres  15641  metres  15642  mopnex  15764  tgioo  15813  cnlimcim  15930  cnlimc  15931  dvfre  15969  dveflem  15985  dvef  15986  efcn  16027  efap1p  16038  sin2pim  16073  cos2pim  16074  sinmpi  16075  cosmpi  16076  sinppi  16077  cosppi  16078  efimpi  16079  sincosq1lem  16085  sincosq2sgn  16087  sincosq3sgn  16088  sincosq4sgn  16089  sinq12gt0  16090  sinq34lt0t  16091  sincosq1eq  16099  abssinper  16106  logrpap0b  16139  loglt1b  16156  rpcxp0  16164  rpcxp1  16165  rpcxpsqrt  16190  logsqrt  16191  rprelogbdiv  16226  ppiqp1le  16300  ppiqeq0  16313  ppiublem1  16324  ppiqub  16326  chtqub  16329  lgs0  16370  lgs2  16374  lgsneg  16381  lgsdilem  16384  lgsdir2lem2  16386  lgsdir2lem4  16388  lgsdir2lem5  16389  lgsne0  16395  2lgslem1a2  16444  2lgslem1c  16447  upgr0eop  16601  uspgrushgr  16659  usgruspgr  16662  usgr0eop  16721  0grsubgr  16743  wlklenvclwlk  16852  upgr2wlkdc  16856  clwwlk0on0  16910  konigsbergssiedgwen  16965  bj-inf2vnlem1  17234  pwle2  17266  pwf1oexmid  17267  domomsubct  17269  nninfsellemeqinf  17298  sbthom  17310  qdiff  17338  iswomninnlem  17339  redc0  17347