Theorem mp2an 761

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp2an.1	|- ph
mp2an.2	|- ps
mp2an.3	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
mp2an	|- ch

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 |- ps
2		mp2an.1	. . 3 |- ph
3		mp2an.3	. . 3 |- ((ph /\ ps) -> ch)
4	2, 3	mpan 759	. 2 |- (ps -> ch)
5	1, 4	ax-mp 7	1 |- ch

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  2false 787  mp3an 1191  eqeq12i 1897  vtocl2 2340  vtocl2OLD 2341  cla42ev 2372  mosub 2433  sbccomg 2526  csbexOLD 2550  sseq12i 2643  uneq12i 2753  ineq12i 2794  keephyp 3027  ralpr 3079  opeq12i 3163  breq12i 3347  opthwiener 3554  opelopab 3570  brab 3571  onsseli 3784  onun2i 3785  snnex 3801  onsucssi 3922  tfis 3938  finds 3979  finds2 3981  xpeq12i 4023  onnev 4070  eqrelriv 4080  eqrelrivOLD 4081  xpex 4096  opelcnv 4143  brcnv 4144  asymref 4308  asymrefOLD 4309  intirrOLD 4313  ssrnres 4354  dfco2 4393  coresOLD 4401  coexg 4429  coex 4430  opabex 4538  fcoi1OLD 4585  fcoi2OLD 4587  fcnvres 4589  fabex 4597  fvopabf 4752  fopabcos 4806  fopabsnOLD 4816  fvi 4818  fvresex 4833  abrexexlem2 4835  iunex 4839  opreq12i 4894  oprabss 4935  oprabex 4948  oprabex2 4950  1st2val 5038  2nd2val 5039  1stconst 5070  2ndconst 5071  fparlem1 5081  fparlem2 5082  fsplit 5086  tz7.44-2 5137  tz7.44-3 5138  tz7.48-2 5166  oawordeulem 5236  oeoalem 5271  oeoa 5272  nneob 5312  ecoprcom 5378  ecoprass 5379  ecoprdi 5380  fnmap 5388  mapval 5391  elmap 5393  elpm 5395  entri 5475  endisj 5496  xpen 5582  pwen 5597  0sdom1dom 5618  xpfi 5632  unfilem1 5641  prfi 5647  unifi 5648  fodomfi 5656  pwfi 5661  pm54.43 5662  ordtypelem1 5684  ordtypelem4 5687  ordtypelem6 5689  ordtype 5691  en2lp 5707  inf0 5712  axinf2 5730  dfom3 5737  oancom 5740  infensuc 5745  trcl 5752  rankr1 5785  rankel 5791  rankss 5799  rankpr 5803  rankval4 5813  rankxplim 5823  rankxplim3 5825  scottex 5846  omsubel 5883  omsubss 5884  aceq3lem 5894  ac6lem 5916  numthlem 5945  zorn2lem1 5950  zorn2lem4 5953  cardon 5976  cardid 5977  carden 5981  unsnen 5985  carddom 5987  cardsdom 5988  domtri 5989  unxpdomlem 5995  unxpdom2 5997  sucxpdom 5998  cardprc 6013  alephsucpw 6018  aleph1 6019  alephord 6023  alephord3 6026  alephgeom 6030  alephfplem1 6044  alephfplem4 6047  alephfp2 6049  alephval2 6050  dominf 6052  cfom 6064  cdavali 6068  uncdadom 6069  pm110.643 6072  cdaen 6073  cda1en 6076  cdacomen 6079  cdaassen 6080  xpcdaen 6081  mapcdaen 6082  cdadom1 6083  cdadom3 6085  cdainf 6087  nnacda 6088  1lt2pi 6184  1q 6209  1lt2pq 6230  halfpq 6234  distrlem5pr 6283  0r 6341  1r 6342  m1r 6343  m1p1sr 6353  m1m1sr 6354  0lt1sr 6356  1ne0sr 6357  1idsr 6359  recexsrlem 6364  mappsrpr 6370  axresscnOLD 6421  axi2m1 6438  addex 6470  mulex 6471  addcli 6473  mulcli 6474  addcomi 6475  mulcomi 6476  readdcli 6487  remulcli 6488  add4i 6496  subcli 6523  subaddi 6528  pncan3i 6535  subnegi 6564  subeq0i 6565  mul4i 6588  muladdi 6589  resubcli 6602  addsub4i 6641  xrltnr 6716  mnfltpnf 6719  lttri2i 6747  lttri3i 6748  letri3i 6749  leloei 6750  ltleni 6751  ltnsymi 6752  lenlti 6753  ltlei 6755  ltsubaddi 6769  lesubaddi 6771  addgt0ii 6781  mulgt0i 6786  mulgt0ii 6788  ltaddposi 6853  posdifi 6854  ltnegcon1i 6855  lenegcon1i 6856  subge0i 6865  recexi 6877  mulne0i 6888  mulnzcnopr 6891  divvali 6893  divmuli 6894  div0i 6947  divmuldivi 6963  divadddivi 6965  divdivdivi 6966  redivcli 6976  recgt0ii 6992  ltdiv23ii 7078  nnssre 7110  nnind 7120  0nnn 7131  2nn 7183  3nn 7184  4nn 7186  1lt3 7214  8th4div3 7217  halfpm6th 7218  xrsupsslem 7285  xrinfmsslem 7286  xrsup0 7306  nn0addcli 7330  nn0mulcli 7331  nn0addge1i 7341  nn0addge2i 7342  halfnz 7406  dfuzi 7414  uzindOLD 7420  ioomax 7561  ioopos 7562  icoshftf1oii 7578  icounlem 7581  snunioolem 7583  eluzaddi 7605  eluzsubi 7606  uzinfmi 7631  fzshftral 7701  om2uzrani 7711  uzrdginii 7715  uzrdgfnuzi 7718  cardfz 7719  seq1val 7725  seq1res 7740  ser1cl1i 7743  ser1recli 7744  ser1refi 7745  ser1monoi 7750  ser1add2i 7751  ser1addi 7752  shftidt 7768  seq1shftid 7769  seq0fval 7778  seqzfval 7780  seqzfn 7782  seq1seqz 7784  seq1seq01 7787  seq1seq0 7788  seq0fn 7789  seq00 7793  serzcl1i 7805  dfseq0 7806  ser0cl1i 7807  ser0fi 7808  sqmuli 7862  sumsqne0i 7879  cu2 7885  expnass 7886  subsqi 7892  nnsqcli 7910  nn0le2msqi 7913  nn0opthlem1 7914  sqr0 7922  sqrlem1 7923  sqrlem2 7924  sqrlem6 7928  sqrlem8 7930  sqrlem13 7935  sqrlem24 7946  sqrgt0ii 7947  sqrlem26 7948  sqrmulii 7954  sqr4 7967  sqr9 7968  sqr2gt1lt2 7969  sqr2irrlem1 7974  sqr2irrlem4 7977  i3 7983  nthruc 7995  nthruz 7996  crrei 8021  crimi 8022  cjmulge0i 8043  abs00i 8093  sqabsaddi 8101  sqabssubi 8102  abstrii 8143  seq1bndi 8162  seq1ublem 8163  seq1ubi 8164  ser1absdiflem 8181  fac1 8187  facp1 8188  faclbnd4lem1 8200  bcpasc2i 8219  bcpasci 8221  fz1fi 8229  sumeq2 8245  fsump1s 8273  csbfsumlem 8286  fsumrev 8289  fsumshft 8291  serzrefi 8311  serzmulci 8318  ser0mulci 8319  ser1mulci 8320  binomlem6 8331  binomi 8332  climunii 8358  climshft2i 8366  climuz0i 8368  climaddci 8392  climmulci 8393  iserzshfti 8404  clim2serzi 8405  climserzlei 8407  climabslem 8408  climubii 8413  climsupi 8415  climcaui 8416  caucvglem2 8418  caucvgi 8423  caucvg3ai 8424  caucvg2i 8425  caucvg3lem 8426  caucvg3 8428  serzf0i 8429  ser1f0i 8430  ser1clim0 8433  ser1cmpi 8434  ser1cmp0i 8435  ser1cmp2i 8437  iserzabslem 8438  cvgcmp2lem 8440  cvgcmp2clem 8442  cvgcmp2clemOLD 8443  cvgcmpubi 8446  cvgcmp3ci 8447  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isumshfti 8465  isumshft2i 8466  isumspliti 8477  isum0spliti 8478  infcvgaux1i 8480  infcvglem2 8483  arisumi 8487  expcnvlem1 8488  expcnvlem2 8489  expcnvlem4 8491  geoseri 8496  geolimilem 8497  geolim1i 8500  georeclim 8502  0.999... 8508  cvgratlem1ALT 8509  cvgratlem2ALT 8510  fsum0diag 8520  fsum0diag2 8521  negfcncfi 8531  abscncflem 8536  ivthlem1 8543  ivthlem4 8546  ivthlem5 8547  ivthlem6 8548  ivthlem7 8549  ivthlem8 8550  ivthlem9 8551  isupivthi 8552  efcltlem1 8566  dfef2i 8569  erelem6 8586  efcji 8598  efaddlem3 8602  efaddlem6 8605  efaddlem7 8606  efaddlem8 8607  efaddlem10 8609  efaddlem12 8611  efaddlem13 8612  efaddlem16 8615  efaddlem17 8616  efaddlem18 8617  efaddlem19 8618  efaddlem20 8619  efaddlem21 8620  efaddlem22 8621  efaddlem25 8624  efaddlem26 8625  efaddlem27 8626  ef1tllem 8643  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  ef01tlubi 8648  absef01tllem 8649  absef01tlubi 8650  eirrlem1 8651  eirrlem2 8652  eirrlem3 8653  eirrlem4 8654  eirrlem5 8655  abspef01tlubi 8660  efsepi 8661  efgt0i 8669  eflti 8671  eflegeolem2 8679  efm1legeoi 8682  efcnlem1 8684  efcn 8688  reeff1olem1 8689  sinaddi 8716  cosaddi 8717  sin01bndlem1 8733  sin01bndlem2 8734  sin01bndlem3 8735  cos01bndlem2 8736  cos01bndlem3 8737  cos1bnd 8740  cos2bnd 8741  sin01gt0 8742  cos01gt0 8743  sin02gt0 8744  sincos1sgn 8745  sincos2sgn 8746  acdc2lem2 8758  acdc5lem2 8761  xpnnen 8768  xpomen 8769  znnen 8771  qnnen 8772  infpn2 8778  ruclem5 8783  ruclem13 8791  ruclem15 8793  ruclem17 8795  ruclem22 8800  ruclem23 8801  ruclem24 8802  ruclem25 8803  ruclem26 8804  ruclem27 8805  ruclem28 8806  ruclem29 8807  ruclem30 8808  ruclem31 8809  ruclem32 8810  ruclem33 8811  ruclem35 8813  ruclem39 8817  resdomq 8819  aleph1re 8820  infxpidmlem9 8829  infxpidmlem12 8832  infcda 8836  infdif 8837  infdif2 8838  infxp 8841  infmap1 8842  iunctb 8844  aleph1irr 8847  qdensere 9027  ismeti 9079  cnmetba 9181  cnmet 9182  cncfmet 9183  cncfmet1 9184  remetba 9187  tgioo 9193  dscmet 9196  lmbrf 9208  iscauf 9217  iscau5 9219  iscaunns 9222  lmsslem 9230  caussi 9232  lmclimnn 9242  xpcn 9254  fsumcnlem 9267  bcth 9310  isgrpi 9322  grprn 9336  grpidvallem 9341  isgrp2i 9360  issubgi 9431  ghgrpilem4 9444  ghsubgi 9446  cnring 9489  ringsn 9490  vsfval 9586  nvcli 9620  cnnvnm 9644  nmcnilem 9676  abscn 9682  abscncfALT 9683  va1cnlem 9684  sm1cnilem 9686  ipid 9702  ipcl 9704  lnocoi 9757  nmlno0lem 9793  nmlno0i 9794  nmblolbi 9800  isblo3i 9801  blocni 9805  blocn 9807  ip0i 9825  ip1ilem 9826  ip2i 9828  ipdirilem 9829  ipasslem1 9831  ipasslem2 9832  ipasslem6 9836  ipasslem7 9837  ipasslem8 9838  ipasslem10 9840  ip2dii 9845  pythi 9851  siilem1 9852  siii 9854  ipblnfi 9857  ajfuni 9861  ubthi 9889  minveclem1 9890  minveclem3 9892  minveclem9 9898  minveclem10 9899  minveclem14 9903  minveclem19 9908  minveclem21 9910  minveclem25 9914  minveclem28 9917  minveclem29 9918  minvecex 9923  minveclem35 9924  minvecdist 9930  minveclem39 9932  htthlem12 9978  spwval2 9996  sincolem 10014  sincnlem 10015  sinco 10016  cosco 10017  pilem1 10020  pilem2 10021  pilem3 10022  pigt2lt4 10024  sinhalfpilem 10028  sincosq1lem 10052  sincosq1sgn 10053  sincosq2sgn 10054  sincosq3sgn 10055  sincosq4sgn 10056  sinq12gt0t 10057  sincos4thpi 10060  sincos6thpi 10061  cosh111lem1 10068  cosh111 10071  efghgrpilem 10073  efif 10075  efifolem1 10076  efifolem2 10077  efifolem3 10078  efifolem4 10079  efifolem5 10080  efifolem6 10081  efifolem7 10082  efif1lem1 10084  efif1lem2 10085  efif1lem3 10086  efif1lem4 10087  efif1lem5 10088  efif1lem6 10089  efif1lem7 10090  circgrp 10094  eff1i 10098  effoi 10099  resslogrn 10107  relogf1o 10111  log1 10120  loge 10121  pilog 10122  emfin 10165  setwoe 10170  elghom 10195  symgval 10202  symggrpi 10205  symgidi 10206  upxp 10225  uptx 10226  txcnopab 10228  2txcn 10229  subsp 10244  ismgm 10367  h2hcau 10481  h2hlm 10482  hvmulex 10513  hvmulcli 10516  hvaddcli 10520  hvcomi 10521  hvsubvali 10522  hvsubcli 10523  hvadd4i 10557  hicli 10581  his1i 10599  normlem6 10614  normlem7 10615  norm-ii.i 10637  normpythi 10642  hhip 10677  hhph 10678  bcsiALT 10679  hlim0 10738  hlimcauii 10739  shsspwh 10751  hhssnm 10764  hhssabli 10765  hhssnv 10767  hhshsslem1 10770  hhshsslem2 10771  hhsssh2 10773  hhssvs 10775  hhssph 10777  occon2i 10795  projlem2 10820  projlem3 10821  projlem4 10822  projlem5 10823  projlem6 10824  projlem8 10826  projlem13 10831  projlem14 10832  projlem15 10833  projlem18 10836  projlem28 10846  pjthlem1 10852  omlsilem 10877  pjpj0i 10888  pjpjthi 10892  pjopi 10895  pjpoi 10896  shseli 10913  shscli 10914  chjvali 10956  shscomi 10965  shsvai 10966  shsel1i 10967  shsel2i 10968  shsleji 10971  shjcomi 10973  shjcli 10977  shlubi 10979  shsumval2i 10993  chsscon3i 11017  chdmm1i 11033  shjshsi 11048  chabs1i 11074  chabs2i 11075  ledii 11092  span0 11098  spanuni 11100  sshhococi 11102  chsup0 11104  h1de2i 11109  spansnpji 11134  pjoml4i 11163  cmbri 11166  fh1i 11197  fh2i 11198  cm2ji 11201  nonbooli 11231  5oai 11241  pjaddii 11255  pjmulii 11257  pjsslem 11259  pjdifnormii 11263  pjneli 11303  mayete3i 11308  mayete3OLDi 11309  mayetes3i 11310  dfiop2 11316  hoeqi 11324  hocofi 11329  hoaddcli 11331  hosubcli 11332  honegsubi 11359  hosubeq0i 11389  ho01i 11391  eigposi 11399  nmopsetn0 11429  nmfnsetn0 11442  hhlnoi 11463  hhnmoi 11464  hhbloi 11465  hh0oi 11466  nmopnegi 11526  0cnfn 11541  0lnfn 11546  nmop0 11547  nmfn0 11548  nmlnop0iALT 11557  lnopco0i 11566  lnopeq0lem1 11567  lnopunilem2 11573  lnophmlem2 11579  nmcopexlem2 11589  lnopconi 11600  lnfn0i 11608  nmcfnexlem2 11618  lnfnconi 11627  nlelshi 11630  cnlnadjlem8 11644  cnlnadjlem9 11645  adjbd1o 11655  bdophsi 11666  bdopcoi 11668  adjcoi 11670  nmopcoadji 11671  unierri 11674  idleop 11702  opsqrlem3 11713  opsqrlem6 11716  hmopidmpji 11724  pjssdif2i 11746  pjssdif1i 11747  pjimai 11748  pjinvari 11764  pjcmmul1i 11774  pjcmmul2i 11775  stcltr1i 11846  mdsl1i 11893  mdslmd1i 11901  mdsldmd1i 11903  mdslmd3i 11904  mdexchi 11907  shatomistici 11933  hatomistici 11934  chpssati 11935  cvati 11938  cvbr3i 11939  cvexchlem 11940  cvexchi 11941  chrelat3i 11944  mdsymlem6 11980  mdsymi 11983  sumdmdii 11987  cmmdi 11988  cmdmdi 11989  sumdmdi 11992  dmdbr4ati 11993  dmdbr6ati 11995  mdcompli 12001  dmdcompli 12002  mddmdin0i 12003  bnj890 12812  bnj922 12834  feq23i 13588  abs2sqlei 13622  abs2sqlti 13623  abs2difi 13626  abs2difabsi 13627  ghomgrpilem1 13628  ghomgrpilem2 13629  ghomsn 13631  cayleylem2 13642  cayleylem3 13643  dvdslelem 13692  divalglem1 13697  divalglem2 13698  divalglem5 13700  divalglem6 13701  divalglem7 13702  divalglem8 13703  divalglem9 13704  gcd0val 13716  gcdaddmlem 13734  algrf 13739  algr0 13740  algrp1 13742  eucalg 13755  mulgcdlem2 13757  mulgcdlem4 13759  mulgcdlem5 13760  1nprm 13769  isprm2lem 13774  isprm3 13776  2prm 13779  4nprm 13781  dfon2lem7 13855  hbimg 13876  wfis 13918  wfis2f 13920  wfis2 13922  trclex 13937  frins 13942  frins2f 13944  noxpsgn 13990  sltval2 13997  axsltsolem1 14006  axdenselem4 14022  axfelem1 14031  fvbigcup 14076  altopth 14095  vxveqv 14357  residcp 14392  eloi 14400  set2elt 14408  ispr1 14496  isprj1 14505  cbicplem 14508  ubos2 14598  ubos 14599  mnlmxl2 14611  prodeq2 14661  fprodp1s 14682  seqzp2 14716  expm 14725  symgfo 14730  zintdom 14787  vecval1b 14794  mapdiscnlem 14870  homcard 14893  eqindhome 14895  top2usne 14898  subspemp 14903  rcfpfillem4 14931  invtrgrp 14979  extopgrp 14980  cntrsetlem 14999  iintlem2 15011  lvsovso 15038  1alg 15069  1ded 15085  0alg 15103  0ded 15104  0cat 15105  1cat 15106  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualded 15132  mrdmcd 15143  cptarc 15242  tmpts 15257  valtar 15260  trclval 15271  isseg1 15304  cbvcsb 15354  cbvsbcOLD 15355  epos 15365  ordtypelem1OLD 15375  ordtypelem4OLD 15378  ordtypelem6OLD 15380  ordtypeOLD 15382  omsubelOLD 15392  omsubssOLD 15393  compfipin0lem 15435  alexsublem4 15440  ivthALT 15454  ufinffr 15578  filnetlem5 15644  mp4an 15651  prfunOLD 15677  difxp 15690  fconst6 15700  opabex3 15701  absrdbnd 15799  elnnr 15803  sdclem1 15809  fdc 15812  fsumltisumii 15822  fsumltisumi 15823  fsumleisumii 15825  csbrni 15832  trirni 15833  trirn 15834  mettrifi 15847  geomcau 15849  caushft 15851  caures 15852  metdcn 15853  iccshftr 15857  iccshftri 15858  iccshftl 15859  iccshftli 15860  iccdil 15861  iccdili 15862  icccntr 15863  icccntri 15864  iiuni 15868  dfii2 15869  dfii3 15870  iirev 15871  iihalf1 15872  iihalf2 15873  iimulcl 15874  lincmb01cmp 15878  lincmb01icc 15879  oprpiece1res1 15880  oprpiece1res2 15881  piececn 15894  cncfres 15895  txtopi 15909  txunii 15910  txcnoprab 15911  cnresoprab 15915  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  txmet 15925  heiborlem6 15960  heiborlem7 15961  heiborlem11 15965  heiborlem12 15966  heiborlem14 15968  heiborlem15 15969  heiborlem16 15970  heiborlem17 15971  heiborlem18 15972  heiborlem30 15984  heiborlem31 15985  heiborlem32 15986  heiborlem33 15987  heiborlem42 15996  bfplem1 15998  bfplem4 16001  bfplem6 16003  bfplem7 16004  bfplem11 16008  bfp 16009  recms 16010  rrntotbnd 16022  ismrer1 16024  reheibor 16025  iicmp 16028  phtpyid 16049  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpyco 16056  reparphtlem2 16064  reparpht 16065  pcoval1 16074  pcoval2 16075  pcocn 16076  pco0 16077  pco1 16078  pcohtpylem1 16080  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1gp 16095  divrngcl 16110  isdivrng2 16111  rnghomval 16118  isrisc 16139  iscring2 16146  eqrelrdv 16251  conss2 16420  addrval 16466  subrval 16467  mulvval 16468  e00an 16636  stb2xpl 16742  stb3xpl 16743  joinfval 16814  meetfval 16821  isgrpiNEW 17115  plusssfval 17204  paddfval 17258

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain