Theorem mp2an 701

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  2false 724  mp3an 922  vtocl2 1889  cla42ev 1916  mosub 1968  sbccomg 2039  csbex 2060  sseq12i 2139  uneq12i 2234  ineq12i 2267  keephyp 2453  opeq12i 2557  breq12i 2701  opthwiener 2884  opelopab 2897  brab 2898  onsseli 3084  onun2i 3085  snnex 3100  onsucssi 3195  tfis 3208  finds 3244  finds2 3246  onnev 3329  eqrelriv 3338  xpex 3349  opelcnv 3389  brcnv 3390  asymref 3531  intirr 3533  ssrnres 3566  dfco2 3598  cores 3602  coexg 3629  coex 3630  opabex 3715  fcoi1 3752  fcoi2 3753  fcnvres 3755  fabex 3761  fvopabf 3900  fopabcos 3947  fopabsn 3954  fvi 3956  fvresex 3971  abrexexlem2 3973  iunex 3977  oprabss 4066  oprabex 4079  oprabex2 4081  1st2val 4158  2nd2val 4159  1stconst 4190  2ndconst 4191  fparlem1 4199  fparlem2 4200  fsplit 4204  tz7.44-2 4230  tz7.44-3 4231  tz7.48-2 4258  oawordeulem 4324  oeoalem 4359  oeoa 4360  nneob 4395  ecoprcom 4460  ecoprass 4461  ecoprdi 4462  fnmap 4470  mapval 4473  elmap 4475  elpm 4477  entri 4557  endisj 4578  xpen 4635  pwen 4650  0sdom1dom 4671  xpfi 4685  unfilem1 4694  prfi 4700  unifi 4701  fodomfi 4709  pwfi 4714  pm54.43 4715  en2lp 4747  inf0 4751  axinf2 4769  dfom3 4776  oancom 4779  infensuc 4784  trcl 4791  rankr1 4820  rankel 4826  rankss 4834  rankpr 4838  rankval4 4848  rankxplim 4858  rankxplim3 4860  scottex 4862  aceq3lem 4878  ac6lem 4900  numthlem 4929  zorn2lem1 4934  zorn2lem4 4937  cardon 4974  cardid 4975  carden 4979  unsnen 4983  carddom 4985  cardsdom 4986  domtri 4987  unxpdomlem 4993  unxpdom2 4995  sucxpdom 4996  cardprc 5011  alephsucpw 5020  aleph1 5021  alephord 5025  alephord3 5028  alephgeom 5032  alephfplem1 5046  alephfplem4 5049  alephfp2 5051  alephval2 5052  dominf 5054  cfom 5066  cdavali 5070  uncdadom 5071  pm110.643 5074  cdaen 5075  cda1en 5078  cdacomen 5081  cdaassen 5082  xpcdaen 5083  mapcdaen 5084  cdadom1 5085  cdadom3 5087  cdainf 5089  nnacda 5090  1lt2pi 5186  1q 5211  1lt2pq 5232  halfpq 5236  distrlem5pr 5285  0r 5343  1r 5344  m1r 5345  m1p1sr 5355  m1m1sr 5356  0lt1sr 5358  1ne0sr 5359  1idsr 5361  recexsrlem 5366  mappsrpr 5372  axresscn 5422  axi2m1 5439  addex 5471  mulex 5472  addcli 5474  mulcli 5475  addcomi 5476  mulcomi 5477  readdcli 5488  remulcli 5489  add4i 5496  subcli 5520  subaddi 5525  pncan3i 5532  subnegi 5558  subeq0i 5559  mul4i 5579  muladdi 5580  resubcli 5593  addsub4i 5628  xrltnr 5695  mnfltpnf 5698  lttri2i 5726  lttri3i 5727  letri3i 5728  leloei 5729  ltleni 5730  ltnsymi 5731  lenlti 5732  ltlei 5734  addgt0ii 5755  mulgt0i 5760  mulgt0ii 5762  ltaddposi 5818  posdifi 5819  ltnegcon1i 5820  lenegcon1i 5821  subge0i 5830  recexi 5841  muln0i 5851  mulnzcnopr 5854  divvali 5856  div0i 5910  divmuldivi 5925  divadddivi 5927  divdivdivi 5928  redivcli 5938  recgt0ii 5954  ltdiv23ii 6040  nnssre 6072  nnind 6082  0nnn 6093  2nn 6145  3nn 6146  4nn 6148  8th4div3 6177  halfpm6th 6178  xrsupsslem 6244  xrinfmsslem 6245  xrsup0 6265  nn0addcli 6289  nn0mulcli 6290  nn0addge1i 6300  nn0addge2i 6301  halfnz 6365  dfuzi 6373  uzindOLD 6379  ioomax 6519  ioopos 6520  icoshftf1oii 6536  icounlem 6539  snunioolem 6541  eluzaddi 6563  eluzsubi 6564  uzinfmi 6589  fzshftral 6653  om2uzrani 6663  uzrdginii 6667  uzrdgfnuzi 6670  cardfz 6671  seq1val 6677  seq1res 6692  ser1cl1i 6695  ser1recli 6696  ser1refi 6697  ser1monoi 6702  ser1add2i 6703  ser1addi 6704  shftidt 6720  seq1shftid 6721  seq0fval 6730  seqzfval 6732  seqzfn 6734  seq1seqz 6736  seq1seq01 6739  seq1seq0 6740  seq0fn 6741  seq00 6745  serzcl1i 6757  dfseq0 6758  ser0cl1i 6759  ser0fi 6760  sqmuli 6814  sumsqne0i 6831  cu2 6837  subsqi 6843  nnsqcli 6861  nn0le2msqi 6864  nn0opthlem1 6865  nn0opthi 6867  sqr0 6873  sqrlem1 6874  sqrlem2 6875  sqrlem6 6879  sqrlem8 6881  sqrlem13 6886  sqrlem24 6897  sqrgt0ii 6898  sqrlem26 6899  sqrmulii 6905  sqr4 6918  sqr9 6919  sqr2gt1lt2 6920  sqr2irrlem1 6925  sqr2irrlem4 6928  i3 6934  nthruc 6946  nthruz 6947  crrei 6972  crimi 6973  cjmulge0i 6994  abs00i 7044  sqabsaddi 7052  sqabssubi 7053  abstrii 7094  seq1bndi 7113  seq1ublem 7114  seq1ubi 7115  ser1absdiflem 7132  fac1 7138  facp1 7139  faclbnd4lem1 7151  bcpasc2i 7170  bcpasci 7172  sumeq2 7188  fsump1s 7216  csbfsumlem 7229  fsumrev 7232  fsumshft 7234  serzrefi 7254  serzmulci 7261  ser0mulci 7262  ser1mulci 7263  binomlem6 7274  binomi 7275  climunii 7301  climshft2i 7309  climuz0i 7311  climaddci 7335  climmulci 7336  iserzshfti 7347  clim2serzi 7348  climserzlei 7350  climabslem 7351  climubii 7356  climsupi 7358  climcaui 7359  caucvglem2 7361  caucvgi 7366  caucvg3ai 7367  caucvg2i 7368  caucvg3lem 7369  caucvg3 7371  serzf0i 7372  ser1f0i 7373  ser1clim0 7376  ser1cmpi 7377  ser1cmp0i 7378  ser1cmp2i 7380  iserzabslem 7381  cvgcmp2lem 7383  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  cvgcmpubi 7389  cvgcmp3ci 7390  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  isumshfti 7408  isumshft2i 7409  isumspliti 7420  isum0spliti 7421  infcvgaux1i 7423  infcvglem2 7426  arisumi 7430  expcnvlem1 7431  expcnvlem2 7432  expcnvlem4 7434  geoseri 7439  geolimilem 7440  geolim1i 7443  georeclim 7445  0.999... 7451  cvgratlem1ALT 7452  cvgratlem2ALT 7453  fsum0diag 7463  fsum0diag2 7464  negfcncfi 7474  abscncflem 7479  ivthlem1 7486  ivthlem4 7489  ivthlem5 7490  ivthlem6 7491  ivthlem7 7492  ivthlem8 7493  ivthlem9 7494  isupivthi 7495  efcltlem1 7509  dfef2i 7512  erelem6 7529  efcji 7541  efaddlem3 7545  efaddlem6 7548  efaddlem7 7549  efaddlem8 7550  efaddlem10 7552  efaddlem12 7554  efaddlem13 7555  efaddlem16 7558  efaddlem17 7559  efaddlem18 7560  efaddlem19 7561  efaddlem20 7562  efaddlem21 7563  efaddlem22 7564  efaddlem25 7567  efaddlem26 7568  efaddlem27 7569  ef1tllem 7586  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  ef01tlubi 7591  absef01tllem 7592  absef01tlubi 7593  eirrlem1 7594  eirrlem2 7595  eirrlem3 7596  eirrlem4 7597  eirrlem5 7598  abspef01tlubi 7603  efsepi 7604  efgt0i 7612  eflti 7614  eflegeolem2 7622  efm1legeoi 7625  efcnlem1 7627  efcn 7631  reeff1olem1 7632  sinaddi 7659  cosaddi 7660  sin01bndlem1 7676  sin01bndlem2 7677  sin01bndlem3 7678  cos01bndlem2 7679  cos01bndlem3 7680  cos1bnd 7683  cos2bnd 7684  sin01gt0 7685  cos01gt0 7686  sin02gt0 7687  sincos1sgn 7688  sincos2sgn 7689  acdc2lem2 7701  acdc5lem2 7704  xpnnen 7711  xpomen 7712  znnen 7714  qnnen 7715  infpn2 7721  ruclem5 7726  ruclem13 7734  ruclem15 7736  ruclem17 7738  ruclem22 7743  ruclem23 7744  ruclem24 7745  ruclem25 7746  ruclem26 7747  ruclem27 7748  ruclem28 7749  ruclem29 7750  ruclem30 7751  ruclem31 7752  ruclem32 7753  ruclem33 7754  ruclem35 7756  ruclem39 7760  resdomq 7762  aleph1re 7763  infxpidmlem9 7772  infxpidmlem12 7775  infcda 7779  infdif 7780  infdif2 7781  infxp 7784  infmap1 7785  iunctb 7787  aleph1irr 7790  qdensere 7961  ismeti 8012  cnmetba 8114  cnmet 8115  cncfmet 8116  cncfmet1 8117  remetba 8120  tgioo 8126  dscmet 8129  lmbrf 8141  iscauf 8150  iscau5 8152  iscaunns 8155  lmsslem 8163  caussi 8165  lmclimnn 8175  xpcn 8187  fsumcnlem 8200  bcth 8243  isgrpi 8255  grprn 8269  grpidvallem 8274  isgrp2i 8293  issubgi 8364  ghgrpilem4 8377  ghsubgi 8379  cnring 8404  ringsn 8405  vsfval 8501  nvcli 8535  cnnvnm 8559  nmcnilem 8591  abscn 8597  abscncfALT 8598  va1cnlem 8599  sm1cnilem 8601  ipid 8617  ipcl 8619  lnocoi 8672  nmlno0lem 8708  nmlno0i 8709  nmblolbi 8715  isblo3i 8716  blocni 8720  blocn 8722  ip0i 8740  ip1ilem 8741  ip2i 8743  ipdirilem 8744  ipasslem1 8746  ipasslem2 8747  ipasslem6 8751  ipasslem7 8752  ipasslem8 8753  ipasslem10 8755  ip2dii 8760  pythi 8766  siilem1 8767  siii 8769  ipblnfi 8772  ajfuni 8776  ubthi 8804  minveclem1 8805  minveclem3 8807  minveclem9 8813  minveclem10 8814  minveclem14 8818  minveclem19 8823  minveclem21 8825  minveclem25 8829  minveclem28 8832  minveclem29 8833  minvecex 8838  minveclem35 8839  minvecdist 8845  minveclem39 8847  htthlem12 8893  spwval2 8915  sincolem 8932  sincnlem 8933  sinco 8934  cosco 8935  pilem1 8938  pilem2 8939  pilem3 8940  pigt2lt4 8942  sinhalfpilem 8946  sincosq1lem 8970  sincosq1sgn 8971  sincosq2sgn 8972  sincosq3sgn 8973  sincosq4sgn 8974  sinq12gt0t 8975  sincos4thpi 8978  sincos6thpi 8979  cosh111lem1 8986  cosh111 8989  efghgrpilem 8991  efif 8993  efifolem1 8994  efifolem2 8995  efifolem3 8996  efifolem4 8997  efifolem5 8998  efifolem6 8999  efifolem7 9000  efif1lem1 9002  efif1lem2 9003  efif1lem3 9004  efif1lem4 9005  efif1lem5 9006  efif1lem6 9007  efif1lem7 9008  circgrp 9012  eff1i 9016  effoi 9017  resslogrn 9025  relogf1o 9029  log1 9038  loge 9039  pilog 9040  h2hcau 9124  h2hlm 9125  hvmulex 9156  hvmulcli 9159  hvaddcli 9163  hvcomi 9164  hvsubvali 9165  hvsubcli 9166  hvadd4i 9200  hicli 9224  his1i 9242  normlem6 9257  normlem7 9258  norm-ii.i 9280  normpythi 9285  hhip 9320  hhph 9321  bcsiALT 9322  hlim0 9381  hlimcauii 9382  shsspwh 9394  hhssnm 9407  hhssabli 9408  hhssnv 9410  hhshsslem1 9413  hhshsslem2 9414  hhsssh2 9416  hhssvs 9418  hhssph 9420  occon2i 9438  projlem2 9463  projlem3 9464  projlem4 9465  projlem5 9466  projlem6 9467  projlem8 9469  projlem13 9474  projlem14 9475  projlem15 9476  projlem18 9479  projlem28 9489  pjthlem1 9495  omlsilem 9520  pjpj0i 9531  pjpjthi 9535  pjopi 9538  pjpoi 9539  shseli 9556  shscli 9557  chjvali 9599  shscomi 9608  shsvai 9609  shsel1i 9610  shsel2i 9611  shsleji 9614  shjcomi 9616  shjcli 9620  shlubi 9622  shsumval2i 9636  chsscon3i 9660  chdmm1i 9676  shjshsi 9691  chabs1i 9717  chabs2i 9718  ledii 9735  span0 9741  spanuni 9743  sshhococi 9745  chsup0 9747  h1de2i 9752  spansnpji 9777  pjoml4i 9806  cmbri 9809  fh1i 9840  fh2i 9841  cm2ji 9844  nonbooli 9874  5oai 9884  pjaddii 9898  pjmulii 9900  pjsslem 9902  pjdifnormii 9906  pjneli 9946  mayete3i 9951  mayete3OLDi 9952  mayetes3i 9953  dfiop2 9959  hoeqi 9967  hocofi 9972  hoaddcli 9974  hosubcli 9975  honegsubi 10002  hosubeq0i 10032  ho01i 10034  eigposi 10042  nmopsetn0 10072  nmfnsetn0 10085  hhlnoi 10106  hhnmoi 10107  hhbloi 10108  hh0oi 10109  nmopnegi 10168  0cnfn 10183  0lnfn 10188  nmop0 10189  nmfn0 10190  nmlnop0iALT 10199  lnopco0i 10208  lnopeq0lem1 10209  lnopunilem2 10215  lnophmlem2 10221  nmcopexlem2 10231  lnopconi 10242  lnfn0i 10250  nmcfnexlem2 10260  lnfnconi 10269  nlelshi 10272  cnlnadjlem8 10286  cnlnadjlem9 10287  adjbd1o 10297  bdophsi 10308  bdopcoi 10310  adjcoi 10312  nmopcoadji 10313  unierri 10316  idleop 10344  hmopidmpji 10360  pjssdif2i 10382  pjssdif1i 10383  pjimai 10384  pjinvari 10400  pjcmmul1i 10410  pjcmmul2i 10411  stcltr1i 10482  mdsl1i 10529  mdslmd1i 10537  mdsldmd1i 10539  mdslmd3i 10540  mdexchi 10543  shatomistici 10569  hatomistici 10570  chpssati 10571  cvati 10574  cvbr3i 10575  cvexchlem 10576  cvexchi 10577  chrelat3i 10580  mdsymlem6 10617  mdsymi 10620  sumdmdii 10624  cmmdi 10625  cmdmdi 10626  sumdmdi 10629  dmdbr4ati 10630  dmdbr6ati 10632  mdcompli 10638  dmdcompli 10639  mddmdin0i 10640  abs2sqle 10657  abs2sqlt 10658  abs2difi 10661  abs2difabsi 10662  elghom 10669  ghomgrpilem1 10670  ghomgrpilem2 10671  ghomsn 10673  symgval 10688  symggrpi 10691  symgidi 10692  cayleylem2 10695  cayleylem3 10696  emfin 10760  vxveqv 10761  residcp 10806  xpeq12i 10816  eloi 10817  set2elt 10827  setwoe 10828  ismgm 10897  seqzp2 10918  expm 10937  mapdiscn 11014  homcard 11045  eqindhome 11047  top2usne 11051  subsp 11056  subspemp 11060  rcfpfillem4 11092  iintlem2 11156  1alg 11176  1ded 11192  0alg 11210  0ded 11211  0cat 11212  1cat 11213  mrdmcd 11249  cbvcsb 11397  cbvsbc 11398  epos 11414  ordtypelem1 11427  ordtypelem4 11430  ordtypelem6 11432  ordtype 11434  omsubel 11444  omsubss 11445  compfipin0lem 11492  alexsublem4 11499  ivthALT 11515  ufinffr 11663  filnetlem5 11767  difxp 11798  opabex3 11806  upxp 11822  absrdbnd 11870  elnnr 11874  sdclem1 11875  fsumltisumii 11885  fsumltisumi 11886  fsumleisumii 11888  fsumleisumi 11889  csbrni 11895  trirni 11896  trirn 11897  mettrifi 11912  geomcau 11914  caushft 11916  caures 11917  metdcn 11918  iccshftr 11922  iccshftri 11923  iccshftl 11924  iccshftli 11925  iccdil 11926  iccdili 11927  icccntr 11928  icccntri 11929  iiuni 11933  dfii2 11934  iirev 11935  iihalf1 11936  iihalf2 11937  iimulcl 11938  lincmb01cmp 11942  lincmb01icc 11943  piececn 11955  cncfres 11956  uptx 11978  txcnopab 11980  txcnoprab 11981  2txcn 11982  heiborlem6 12016  heiborlem7 12017  heiborlem11 12021  heiborlem12 12022  heiborlem14 12024  heiborlem15 12025  heiborlem16 12026  heiborlem17 12027  heiborlem18 12028  heiborlem30 12040  heiborlem31 12041  heiborlem32 12042  heiborlem33 12043  heiborlem42 12052  bfplem1 12054  bfplem4 12057  bfplem6 12059  bfplem7 12060  bfplem11 12064  bfp 12065  recms 12066  rrntotbnd 12078  ismrer1 12080  reheibor 12081  iicmp 12084  phtpyid 12091  phtpycom 12092  phtpycolem1 12093  phtpycolem2 12094  phtpycolem3 12095  phtpycolem4 12096  phtpycolem5 12097  phtpyco 12098

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 145  df-an 223

Copyright terms: Public domain