Theorem mp2an 681

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 677	. 2 |- (ps -> ch)
5	1, 4	ax-mp 7	1 |- ch

Syntax hints:   -> wi 3   /\ wa 337

This theorem is referenced by:  mp4an 682  mp3an 1466  eqeq12i 2154  vtocl2 2584  cla42ev 2612  mosub 2678  sbccomg 2758  sseq12i 2870  uneq12i 2971  ineq12i 3007  keephyp 3221  ralpr 3272  preq12i 3293  opeq12i 3350  breq12i 3516  opthwiener 3717  opelopab 3731  brab 3732  onsseli 3924  onun2i 3925  snnex 3940  onsucssi 4062  tfis 4075  finds 4112  finds2 4114  xpeq12i 4156  onnevOLD 4203  eqrelriiv 4213  xpex 4226  opelcnv 4270  brcnv 4271  asymref 4423  ssrnres 4460  dfco2 4495  coexg 4533  coex 4534  opabex 4635  feq23i 4656  fcnvres 4680  fabex 4686  fvopabf 4838  fopabcos 4898  fvi 4910  fvresex 4926  abrexexlem2 4928  opabex3 4933  iunex 4934  opreq12i 4991  oprabid 5002  oprabss 5028  oprabex 5041  oprabex2 5043  1st2val 5144  2nd2val 5145  difxp 5151  1stconst 5193  2ndconst 5194  fparlem1 5204  fparlem2 5205  fsplit 5209  tz7.44-2 5301  tz7.44-3 5302  tz7.48-2 5329  tz7.48-2OLD 5330  oawordeulem 5399  oeoalem 5437  oeoa 5438  nneob 5473  ecoprcom 5539  ecoprass 5540  ecoprdi 5541  fnmap 5549  mapval 5552  elmap 5554  elpm 5556  entri 5636  endisj 5660  xpen 5767  xpenOLD 5768  pwen 5788  infensuc 5793  0sdom1dom 5813  1sdom 5815  unxpdom2 5821  sucxpdom 5822  isinf 5828  xpfir 5838  0fin 5839  en1eqsn 5840  unfilem1 5860  prfi 5869  unifi 5870  fodomfi 5880  pwfi 5885  pm54.43 5886  ordtypelem1 5915  ordtypelem4 5918  ordtypelem6 5920  ordtype 5922  en2lp 5939  inf0 5944  axinf2 5963  dfom3 5972  oancom 5976  infensucOLD 5981  trcl 5988  rankr1 6021  rankel 6027  rankss 6035  rankpr 6039  rankval4 6049  rankxplim 6059  rankxplim3 6061  scottex 6085  carden2b 6122  carddom2 6132  leweon 6145  infxpidm2 6149  xpomen 6150  alephord 6160  alephord2 6161  alephord3 6163  alephgeom 6164  omsubel 6174  omsubss 6175  aceq3lem 6186  aceq8alem 6198  alephnbtwn2 6210  alephsucdom 6211  alephf1ALT 6226  alephfplem1 6227  alephfplem4 6230  alephfp2 6232  cdavali 6238  uncdadom 6239  pm110.643 6243  cdaen 6244  cdacomen 6249  cdaassen 6250  mapcdaen 6252  cdadom1 6253  cdadom3 6255  cardacda 6260  nnaun 6262  nnaun2 6263  pwsdompw 6264  cfsmolem 6285  axcc2lem 6293  dcomex 6302  axdc3lem4 6308  axdc4lem 6310  ac6lem 6324  numthlem 6355  zorn2lem1 6361  zorn2lem4 6364  axdclem2 6372  cardonOLD 6390  cardid 6391  carden 6395  unsnen 6399  carddom 6401  cardsdom 6402  domtri 6403  unxpdomlemOLD 6410  infxpidm 6416  cardprcOLD 6426  konigthlem 6429  alephsucpw 6434  aleph1 6435  alephordOLD 6439  alephval2 6444  dominfac 6445  cfomOLD 6448  alephreg 6449  pwcfsdom 6450  cfpwsdom 6451  cdainfOLD 6454  nnacdaOLD 6455  1lt2pi 6550  1q 6575  halfpq 6600  distrlem5pr 6649  0r 6707  1sr 6708  m1r 6709  m1p1sr 6719  m1m1sr 6720  0lt1sr 6722  1ne0sr 6723  1idsr 6725  recexsrlem 6730  mappsrpr 6736  axi2m1 6801  addex 6821  mulex 6822  addcli 6824  mulcli 6825  mulcomi 6826  readdcli 6835  remulcli 6836  xrltnr 6900  mnfltpnf 6903  lttri2i 6931  lttri3i 6932  letri3i 6933  leloei 6934  ltleni 6935  ltnsymi 6936  lenlti 6937  ltlei 6939  mulgt0i 6950  mulgt0ii 6951  subcli 7019  subaddi 7024  pncan3i 7031  subnegi 7057  subeq0i 7058  resubcli 7079  ltsubaddi 7123  lesubaddi 7124  addgt0ii 7130  ltaddposi 7186  posdifi 7187  ltnegcon1i 7188  lenegcon1i 7189  subge0i 7198  recexi 7209  mulnzcnopr 7222  divvali 7224  divmuli 7225  div0i 7278  divadddivi 7296  redivcli 7307  recgt0ii 7323  ltdiv23ii 7411  nnssre 7443  nnind 7453  0nnn 7464  2nn 7516  3nn 7517  4nn 7519  9nn 7545  1lt3 7550  1lt6 7551  8th4div3 7557  halfpm6th 7558  xrsupsslem 7625  xrinfmsslem 7626  nn0addcli 7671  nn0mulcli 7672  nn0addge1i 7682  nn0addge2i 7683  halfnz 7749  dfuzi 7757  uzindOLD 7763  ioomax 7907  ioopos 7908  icoshftf1oii 7924  icounlem 7927  snunioolem 7929  eluzaddi 7952  eluzsubi 7953  uzinfmi 7986  fseq1p1m1lem2 8063  fseq1p1m1lem3 8064  fzshftral 8072  om2uzrani 8082  uzrdginii 8086  uzrdgfnuzi 8089  fzennn 8090  cardfzOLD 8092  seq1val 8098  seq1res 8113  ser1cl1i 8118  ser1recli 8119  ser1refi 8120  ser1monoi 8125  ser1add2i 8126  ser1addi 8127  shftidt 8143  seq1shftid 8144  seq0fval 8153  seqzfval 8155  seqzfn 8157  seq1seqz 8159  seq1seq01 8162  seq1seq0 8163  seq0fn 8164  seq00 8168  serzcl1i 8189  dfseq0 8190  ser0cl1i 8191  ser0fi 8192  sqmuli 8246  sumsqne0i 8263  cu2 8269  expnass 8270  subsqi 8276  nnsqcli 8294  nn0le2msqi 8297  nn0opthlem1 8298  sqr0 8306  sqrlem1 8307  sqrlem2 8308  sqrlem6 8312  sqrlem8 8314  sqrlem13 8319  sqrlem24 8330  sqrgt0ii 8331  sqrlem26 8332  sqrmulii 8338  sqr4 8351  sqr9 8352  sqr2gt1lt2 8353  sqr2irrlem1 8358  sqr2irrlem4 8361  i3 8367  nthruc 8379  nthruz 8380  crrei 8405  crimi 8406  cjmulge0i 8427  abs00i 8477  sqabsaddi 8485  sqabssubi 8486  abstrii 8527  seq1bndi 8547  seq1ublem 8548  seq1ubi 8549  ser1absdiflem 8566  fac1 8572  facp1 8573  faclbnd4lem1 8585  bcpasc2i 8604  bcpasci 8606  fz1fiOLD 8615  hashsng 8627  hashsngOLD 8628  sumeq2 8641  fsump1s 8669  csbfsumlem 8682  fsumrev 8685  fsumshft 8687  serzrefi 8707  serzmulci 8714  ser0mulci 8715  ser1mulci 8716  binomlem6 8727  binomi 8728  climunii 8754  climshft2i 8762  climuz0i 8764  climaddci 8788  climmulci 8789  iserzshfti 8800  clim2serzi 8801  climserzlei 8803  climabslem 8804  climubii 8809  climsupi 8811  climcaui 8812  caucvglem2 8814  caucvgi 8819  caucvg3ai 8820  caucvg2i 8821  caucvg3lem 8822  caucvg3 8824  serzf0i 8825  ser1f0i 8826  ser1clim0 8829  ser1cmpi 8830  ser1cmp0i 8831  ser1cmp2i 8833  iserzabslem 8834  cvgcmp2lem 8836  cvgcmp2clem 8838  cvgcmp2clemOLD 8839  cvgcmpubi 8842  cvgcmp3ci 8843  cvgcmp3cetlem1 8845  cvgcmp3cetlem2 8846  isumshfti 8861  isumshft2i 8862  isumspliti 8873  isum0spliti 8874  supcvglem 8876  infcvgaux1i 8878  arisumi 8885  expcnvlem1 8886  expcnvlem2 8887  expcnvlem4 8889  geoseri 8894  geolimilem 8895  geolim1i 8898  georeclim 8900  0.999... 8906  cvgratlem1ALT 8907  cvgratlem2ALT 8908  fsum0diag 8918  fsum0diag2 8919  negfcncfi 8929  abscncflem 8934  ivthlem1 8941  ivthlem4 8944  ivthlem5 8945  ivthlem6 8946  ivthlem7 8947  ivthlem8 8948  ivthlem9 8949  isupivthi 8950  efcltlem1 8964  dfef2i 8967  erelem6 8984  efcji 8996  efaddlem3 9000  efaddlem6 9003  efaddlem7 9004  efaddlem8 9005  efaddlem10 9007  efaddlem12 9009  efaddlem13 9010  efaddlem16 9013  efaddlem17 9014  efaddlem18 9015  efaddlem19 9016  efaddlem20 9017  efaddlem21 9018  efaddlem22 9019  efaddlem25 9022  ef1tllem 9041  ef01tllem1 9043  ef01tllem2 9044  ef01tllem2OLD 9045  ef01tlubi 9046  absef01tllem 9047  absef01tlubi 9048  eirrlem1 9049  eirrlem2 9050  eirrlem3 9051  eirrlem4 9052  eirrlem5 9053  abspef01tlubi 9058  efsepi 9059  efgt0i 9067  eflegeolem2 9077  efm1legeoi 9080  efcnlem1 9082  efcn 9086  reeff1olem1 9087  sin01bndlem1 9131  sin01bndlem2 9132  sin01bndlem3 9133  cos01bndlem2 9134  cos01bndlem3 9135  cos1bnd 9138  cos2bnd 9139  sin01gt0 9140  cos01gt0 9141  sin02gt0 9142  sincos1sgn 9143  sincos2sgn 9144  acdc2lem2 9156  acdc5lem2 9159  xpnnen 9166  xpnnenOLD 9167  xpomenOLD 9168  znnen 9170  qnnen 9171  qnnenOLD 9172  ruclem5 9177  ruclem13 9185  ruclem15 9187  ruclem17 9189  ruclem22 9194  ruclem23 9195  ruclem24 9196  ruclem25 9197  ruclem26 9198  ruclem27 9199  ruclem28 9200  ruclem29 9201  ruclem30 9202  ruclem31 9203  ruclem32 9204  ruclem33 9205  ruclem35 9207  ruclem39 9211  resdomq 9213  aleph1re 9214  infxpidmlem9OLD 9223  infxpidmlem12OLD 9226  infcda 9230  infdif 9231  infdif2 9232  infxp 9235  infmap1 9236  iunctb 9238  aleph1irr 9241  dvdslelem 9285  divalglem1 9291  divalglem2 9292  divalglem5 9294  divalglem6 9295  divalglem7 9296  divalglem8 9297  divalglem9 9298  gcd0val 9310  gcdaddmlem 9328  algrf 9334  algr0 9335  algrp1 9337  eucalg 9350  mulgcdlem2 9352  mulgcdlem4 9354  mulgcdlem5 9355  1nprm 9366  isprm2lem 9368  isprm3 9370  2prm 9374  4nprm 9376  exprmfctlem 9380  infpn2 9391  prminf 9393  isgrpi 9480  joinfval 9581  meetfval 9588  txtopi 9793  txunii 9795  qdensere 9893  ismeti 9945  cnmetba 10047  cnmet 10048  cncfmet 10049  cncfmet1 10050  remetba 10053  dscmet 10062  lmbrf 10074  iscauf 10083  iscau5 10085  iscaunns 10088  lmsslem 10096  caussi 10098  lmclimnn 10108  xpcn 10120  fsumcnlem 10133  bcth 10176  grp2grpo 10190  isgrpoi 10191  grprn 10205  grpidvallem 10210  isgrp2i 10229  issubgi 10300  ghgrpilem4 10313  ghsubgi 10315  cnring 10358  ringsn 10359  vsfval 10455  nvcli 10489  cnnvnm 10513  nmcnilem 10545  abscn 10551  abscncfALT 10552  va1cnlem 10553  sm1cnilem 10555  ipid 10571  ipcl 10573  lnocoi 10626  nmlno0lem 10662  nmlno0i 10663  nmblolbi 10669  isblo3i 10670  blocni 10674  blocn 10676  ip0i 10694  ip1ilem 10695  ip2i 10697  ipdirilem 10698  ipasslem1 10700  ipasslem2 10701  ipasslem6 10705  ipasslem7 10706  ipasslem8 10707  ipasslem10 10709  ip2dii 10714  pythi 10720  siilem1 10721  siii 10723  ipblnfi 10726  ajfuni 10730  ubthi 10758  minveclem1 10759  minveclem3 10761  minveclem9 10767  minvec34 10768  minveclem10 10769  minveclem14 10773  minveclem19 10778  minveclem21 10780  minveclem25 10784  minveclem28 10787  minveclem29 10788  minvecex 10793  minvecexOLD 10794  minveclem35 10795  minvecdist 10801  minveclem39 10803  htthlem12 10849  spwval2 10867  sincolem 10885  sincnlem 10886  sinco 10887  cosco 10888  pilem1 10891  pilem2 10892  pilem3 10893  pigt2lt4 10895  sinhalfpilem 10899  sincosq1lem 10923  sincosq1sgn 10924  sincosq2sgn 10925  sincosq3sgn 10926  sincosq4sgn 10927  sinq12gt0t 10928  sincos4thpi 10931  sincos6thpi 10932  cosh111lem1 10939  cosh111 10942  efghgrpilem 10944  efif 10946  efifolem1 10947  efifolem2 10948  efifolem3 10949  efifolem4 10950  efifolem5 10951  efifolem6 10952  efifolem7 10953  efif1lem1 10955  efif1lem2 10956  efif1lem3 10957  efif1lem4 10958  efif1lem5 10959  efif1lem6 10960  efif1lem7 10961  circgrp 10965  eff1i 10969  effoi 10970  resslogrn 10978  relogf1o 10982  log1 10991  loge 10992  pilog 10993  symgval 11034  symggrpi 11037  symgidi 11038  upxp 11060  uptx 11061  txcnopab 11063  2txcn 11064  subspi 11079  h2hcau 11319  h2hlm 11320  hvmulex 11351  hvmulcli 11354  hvaddcli 11358  hvcomi 11359  hvsubvali 11360  hvsubcli 11361  hicli 11418  his1i 11436  normlem6 11451  normlem7 11452  norm-ii.i 11473  normpythi 11478  hhip 11513  hhph 11514  bcsiALT 11515  hlim0 11572  hlimcauii 11573  shsspwh 11585  hhssnm 11598  hhssabli 11599  hhssnv 11601  hhshsslem1 11604  hhshsslem2 11605  hhsssh2 11607  hhssvs 11609  hhssph 11611  occon2i 11629  projlem2 11654  projlem3 11655  projlem4 11656  projlem5 11657  projlem6 11658  projlem8 11660  projlem13 11665  projlem14 11666  projlem15 11667  projlem18 11670  projlem28 11680  pjthlem1 11686  pjpj0i 11722  pjpjthi 11726  pjopi 11729  pjpoi 11730  shseli 11747  shscli 11748  chjvali 11790  shscomi 11799  shsvai 11800  shsel1i 11801  shsel2i 11802  shsvsi 11803  shsleji 11805  shjcomi 11807  shjcli 11811  shlubi 11813  shsumval2i 11827  chsscon3i 11851  chdmm1i 11867  shjshsi 11882  chabs1i 11908  chabs2i 11909  ledii 11926  span0 11932  spanuni 11934  sshhococi 11936  chsup0 11938  h1de2i 11943  spansnpji 11968  pjoml4i 11995  cmbri 11998  fh1i 12029  fh2i 12030  cm2ji 12033  nonbooli 12063  5oai 12073  pjaddii 12087  pjmulii 12089  pjsslem 12091  pjdifnormii 12095  pjneli 12135  mayete3i 12140  mayete3OLDi 12141  mayetes3i 12142  dfiop2 12148  hoeqi 12156  hocofi 12161  hoaddcli 12163  hosubcli 12164  honegsubi 12191  hosubeq0i 12221  ho01i 12223  eigposi 12231  nmopsetn0 12261  nmfnsetn0 12274  hhlnoi 12295  hhnmoi 12296  hhbloi 12297  hh0oi 12298  nmopnegi 12358  0cnfn 12373  0lnfn 12378  nmop0 12379  nmfn0 12380  nmlnop0iALT 12389  lnopco0i 12398  lnopeq0lem1 12399  lnopunilem2 12405  lnophmlem2 12411  lnopconi 12432  lnfn0i 12440  lnfnconi 12459  nlelshi 12462  cnlnadjlem8 12476  cnlnadjlem9 12477  adjbd1o 12487  adjcoi 12502  nmopcoadji 12503  unierri 12506  idleop 12533  opsqrlem3 12544  opsqrlem6 12547  hmopidmpji 12555  pjssdif2i 12577  pjssdif1i 12578  pjimai 12579  pjinvari 12595  pjcmmul1i 12605  pjcmmul2i 12606  stcltr1i 12677  mdsl1i 12724  mdslmd1i 12732  mdsldmd1i 12734  mdslmd3i 12735  mdexchi 12738  shatomistici 12764  hatomistici 12765  chpssati 12766  cvati 12769  cvbr3i 12770  cvexchlem 12771  cvexchi 12772  chrelat3i 12775  mdsymlem6 12811  mdsymi 12814  sumdmdii 12818  cmmdi 12819  cmdmdi 12820  sumdmdi 12823  dmdbr4ati 12824  dmdbr6ati 12826  mddmdin0i 12834  bnj890 13583  bnj922 13605  hashxplem 14361  hashpw 14364  ghomgrpilem1 14365  ghomgrpilem2 14366  ghomsn 14368  cayleylem2 14379  cayleylem3 14380  sindivcvglem1 14386  sindivcvglem2 14387  sindivcvglem3 14388  sindivcvglem4 14389  circumlem2 14396  circumlem3 14397  abs2sqlei 14414  abs2sqlti 14415  abs2difi 14418  abs2difabsi 14419  dfon2lem7 14489  nnacli 14496  nnmcli 14497  omopthlem1 14501  omopthlem2 14502  omopthi 14503  hbimg 14517  wfis 14563  wfis2f 14565  wfis2 14567  trpred0 14588  trpredex 14589  frins 14595  frins2f 14597  sltval2 14662  noxpsgn 14671  axsltsolem1 14674  axdenselem4 14691  axfelem2 14700  fobigcup 14761  fvbigcup 14763  elfuns 14774  dfiota3 14777  altopth 14792  altopthb 14793  vxveqv 15067  residcp 15102  prj1b 15105  prj3 15106  eloi 15112  set2elt 15120  ispr1 15235  isprj1 15244  cbicplem 15247  ubos2 15337  ubos 15338  mnlmxl2 15350  prodeq2 15400  fprodp1s 15421  seqzp2 15451  expm 15460  symgfo 15465  zintdom 15540  vecval1b 15547  homcard 15650  eqindhome 15652  top2usne 15655  intopcoaconlem3 15660  intopcoaconb 15662  intopcoaconc 15663  subspemp 15665  rcfpfillem4 15697  invtrgrp 15757  extopgrp 15758  cntrsetlem 15791  iintlem2 15803  lvsovso 15832  1alg 15863  1ded 15879  0alg 15897  0ded 15898  0cat 15899  1cat 15900  dualcat2lem 15923  dualded2lem 15924  dualalg 15925  dualded 15926  mrdmcd 15937  cptarc 16052  tmpts 16067  valtar 16070  trclval 16081  isseg1 16114  cbvcsb 16178  cbvsbcOLD 16179  epos 16189  ordtypelem1OLD 16199  ordtypelem4OLD 16202  ordtypelem6OLD 16204  ordtypeOLD 16206  omsubelOLD 16216  omsubssOLD 16217  compfipin0lem 16259  alexsublem4 16264  ivthALT 16278  ufinffr 16402  filnetlem5 16468  prfunOLD 16501  difxpOLD 16514  fconst6 16524  opabex3OLD 16525  absrdbnd 16623  elnnr 16627  sdclem1 16633  fdc 16636  fsumltisumii 16646  fsumltisumi 16647  fsumleisumii 16649  csbrni 16656  trirni 16657  trirn 16658  mettrifi 16671  geomcau 16673  caushft 16675  metdcn 16677  iccshftri 16682  iccshftli 16684  iccdili 16686  icccntri 16688  iiuni 16692  dfii2 16693  dfii3 16694  iirev 16695  iihalf1 16696  iihalf2 16697  iimulcl 16698  lincmb01cmp 16702  lincmb01icc 16703  oprpiece1res1 16704  oprpiece1res2 16705  piececn 16718  cncfres 16719  txtopiOLD 16733  txuniiOLD 16734  txcnoprab 16735  cnresoprab 16739  cnopropabco 16741  cnoproprabco 16743  cnoprab1 16745  cnoprab2 16746  txmet 16749  heiborlem6 16784  heiborlem7 16785  heiborlem11 16789  heiborlem12 16790  heiborlem14 16792  heiborlem15 16793  heiborlem16 16794  heiborlem17 16795  heiborlem18 16796  heiborlem30 16808  heiborlem31 16809  heiborlem32 16810  heiborlem33 16811  heiborlem42 16820  bfplem1 16822  bfplem4 16825  bfplem6 16827  bfplem7 16828  bfplem11 16832  bfp 16833  recms 16834  rrntotbnd 16846  ismrer1 16848  reheibor 16849  iicmp 16852  phtpyid 16873  phtpycom 16874  phtpycolem1 16875  phtpycolem2 16876  phtpycolem3 16877  phtpycolem4 16878  phtpycolem5 16879  phtpyco 16880  reparphtlem2 16888  reparpht 16889  pcoval1 16898  pcoval2 16899  pcocn 16900  pco0 16901  pco1 16902  pcohtpylem1 16904  pcohtpylem2 16905  pcohtpylem3 16906  pcohtpy 16907  pcopt 16908  pcoass 16909  pcorevlem 16910  pcorev 16911  pi1gp 16919  divrngcl 16934  isdivrng2 16935  rnghomval 16942  isrisc 16963  iscring2 16970  eqrelrdv 17075  conss2 17244  addrval 17288  subrval 17289  mulvval 17290  e00an 17470  plusssfval 17916  paddfval 18229

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 220  df-an 339

Copyright terms: Public domain