Theorem mp2an 695

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  2false 717  mp3an 913  vtocl2 1834  cla42ev 1861  mosub 1913  sbccomg 1979  csbex 1999  sseq12i 2077  uneq12i 2172  ineq12i 2205  keephyp 2386  opeq12i 2483  breq12i 2618  opthwiener 2796  opelopab 2809  brab 2810  ideqOLD 2828  onssel 3099  onun 3100  onsucss 3101  tfis 3117  finds 3146  finds2 3148  onnev 3232  eqrelriv 3241  xpex 3250  opelcnv 3287  brcnv 3288  asymref 3423  asymrefOLD 3425  intirr 3427  ssrnres 3467  cores 3485  coexg 3510  coex 3511  opabex 3595  fcoi1 3630  fcoi2 3631  fcnvres 3633  fabex 3639  fvopabf 3774  fopabcos 3818  fopabsn 3825  fvi 3827  fvresex 3842  abrexexlem2 3844  iunex 3848  tz7.44-2 3914  tz7.44-3 3915  tz7.48-2 3942  oprabss 3991  oprabex 4004  oprabex2 4006  1st2val 4079  2nd2val 4080  2ndconst 4081  df1st2 4110  df2nd2 4111  oawordeulem 4172  nneob 4239  ecoprcom 4303  ecoprass 4304  ecoprdi 4305  fnmap 4313  mapval 4316  elmap 4318  elpm 4320  entr 4397  endisj 4417  2pwuninel 4465  xpen 4468  pwen 4483  0sdom1dom 4504  unfilem1 4524  prfi 4531  fodomfi 4540  pwfi 4545  pm54.43 4546  en2lp 4574  inf0 4578  axinf2 4596  dfom3 4602  oancom 4605  infensuc 4610  trcl 4617  rankr1 4646  rankel 4652  rankss 4660  rankpr 4664  rankval4 4674  rankxplim 4684  rankxplim3 4686  scottex 4688  aceq3lem 4704  ac6lem 4726  numthlem 4755  zorn2lem1 4760  zorn2lem4 4763  cardon 4799  cardid 4800  carden 4803  carddom 4808  cardsdom 4809  domtri 4810  unxpdomlem 4815  unxpdom2 4817  sucxpdom 4818  cardprc 4833  alephsucpw 4842  aleph1 4843  alephord 4847  alephord3 4850  alephgeom 4854  alephfplem1 4868  alephfplem4 4871  alephfp2 4873  alephval2 4874  dominf 4876  cfom 4888  cdaval 4892  uncdadom 4893  pm110.643 4895  cdaen 4896  cda1en 4898  cdacomen 4901  cdaassen 4902  xpcdaen 4903  mapcdaen 4904  cdadom1 4905  cdadom3 4907  cdainf 4909  1lt2pi 5004  1q 5029  1lt2pq 5050  halfpq 5054  distrlem5pr 5103  0r 5161  1r 5162  m1r 5163  m1p1sr 5173  m1m1sr 5174  0lt1sr 5176  1ne0sr 5177  1idsr 5179  recexsrlem 5184  mappsrpr 5190  axresscn 5240  axi2m1 5257  addex 5289  mulex 5290  addcl 5292  mulcl 5293  addcom 5294  mulcom 5295  readdcl 5306  remulcl 5307  add4 5314  subcl 5338  subadd 5343  pncan3 5350  subneg 5376  subeq0 5377  mul4 5397  muladd 5398  resubcl 5411  addsub4 5446  xrltnrt 5514  mnfltpnf 5517  lttri2 5545  lttri3 5546  letri3 5547  leloe 5548  ltlen 5549  ltnsym 5550  lenlt 5551  ltle 5553  ltneOLD 5557  addgt0i 5575  mulgt0 5580  mulgt0i 5582  ltaddpos 5637  posdif 5638  ltnegcon1 5639  lenegcon1 5640  subge0 5649  recex 5658  muln0 5668  mulnzcnopr 5671  divval 5673  div0 5727  divmuldiv 5742  divadddiv 5744  divdivdiv 5745  redivcl 5754  recgt0i 5770  ltdiv23i 5843  nnssre 5875  nnind 5885  0nnn 5896  2nn 5946  3nn 5947  4nn 5949  8th4div3 5978  halfpm6th 5979  xrsupsslem 6023  xrinfmsslem 6024  xrsup0 6044  nn0addcl 6068  nn0mulcl 6069  nn0addge1 6079  nn0addge2 6080  halfnz 6141  dfuz 6150  uzindOLD 6156  om2uzran 6237  uzrdgini 6240  uzrdgfnuz 6243  seq1val 6249  seq1res 6264  ser1cl1 6267  ser1recl 6268  ser1ref 6269  ser1mono 6274  ser1add2 6275  ser1add 6276  shftidt 6292  seq1shftid 6293  ioomax 6325  ioopos 6326  icoshftf1oi 6342  icounlem 6345  snunioolem 6347  eluzaddi 6368  eluzsubi 6369  uzinfm 6394  fzshftralt 6454  seq0fval 6467  seqzfval 6469  seqzfn 6471  seq1seqz 6473  seq1seq0t 6476  seq1seq0 6477  seq0fn 6478  seq00 6482  serzcl1 6494  dfseq0 6495  ser0cl1 6496  ser0f 6497  sqmul 6547  sumsqne0 6565  cu2 6571  subsq 6577  nnsqcl 6590  nn0le2msqt 6593  nn0opthlem1 6594  nn0opth 6596  sqr0 6602  sqrlem1 6603  sqrlem2 6604  sqrlem6 6608  sqrlem8 6610  sqrlem13 6615  sqrlem24 6626  sqrgt0i 6627  sqrlem26 6628  sqrmuli 6634  sqr4 6647  sqr9 6648  sqr2gt1lt2 6649  sqr2irrlem1 6654  sqr2irrlem4 6657  i3 6663  nthruc 6676  nthruz 6677  crre 6706  crreOLD 6707  crim 6708  crimOLD 6709  cjmulge0 6728  abs00 6777  sqabsadd 6785  sqabssub 6786  abstri 6829  seq1bnd 6847  seq1ublem 6848  seq1ub 6849  ser1absdiflem 6866  fac1 6872  facp1t 6873  faclbnd4lem1 6885  bcpasc2 6905  bcpasc 6907  sumeq2 6923  fsump1s 6951  csbfsumlem 6964  fsumrev 6967  fsumshft 6969  serzref 6989  serzmulc 6996  ser0mulc 6997  ser1mulc 6998  binomlem6 7009  binom 7010  climunii 7035  climshft2 7043  climuz0 7045  climaddc 7068  climmulc 7069  iserzshft 7080  clim2serz 7081  climserzle 7083  climabslem 7084  climubi 7089  climsup 7091  climcau 7092  caucvglem2 7094  caucvg 7099  caucvg3a 7100  caucvg2 7101  caucvg3lem 7102  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1clim0 7109  ser1cmp 7110  ser1cmp0 7111  ser1cmp2 7113  iserzabslem 7114  cvgcmp2lem 7116  cvgcmp2clem 7118  cvgcmpub 7121  cvgcmp3c 7122  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isumshft 7139  isumshft2 7140  isumsplit 7151  isum0split 7152  infcvgaux1 7154  infcvglem2 7157  fnsmnt 7161  expcnvlem1 7162  expcnvlem2 7163  expcnvlem4 7165  geoser 7169  geolimilem 7170  geolim1i 7173  georeclim 7175  0.999... 7181  cvgratlem1ALT 7182  cvgratlem2ALT 7183  fsum0diag 7193  fsum0diag2 7194  negfcncf 7204  abscncflem 7209  ivthlem1 7216  ivthlem4 7219  ivthlem5 7220  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem9 7224  isupivth 7225  ivthlem4OLD 7228  ivthlem5OLD 7229  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  ivthOLD 7233  ivth2OLD 7234  efcltlem1 7246  dfef2 7249  erelem6 7266  efcj 7278  efaddlem3 7282  efaddlem6 7285  efaddlem7 7286  efaddlem8 7287  efaddlem10 7289  efaddlem12 7291  efaddlem13 7292  efaddlem16 7295  efaddlem17 7296  efaddlem18 7297  efaddlem19 7298  efaddlem20 7299  efaddlem21 7300  efaddlem22 7301  efaddlem25 7304  efaddlem26 7305  efaddlem27 7306  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  ef01tlub 7327  absef01tllem 7328  absef01tlub 7329  eirrlem1 7330  eirrlem2 7331  eirrlem3 7332  eirrlem4 7333  eirrlem5 7334  abspef01tlub 7336  efsep 7337  efgt0 7345  eflt 7347  eflegeolem2 7354  efm1legeo 7357  efcnlem1 7359  efcn 7363  reeff1olem1 7364  reeff1olem1OLD 7366  sinadd 7393  cosadd 7394  sin01bndlem1 7409  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  cos1bnd 7416  cos2bnd 7417  sin01gt0 7418  cos01gt0 7419  sin02gt0 7420  sincos1sgn 7421  sincos2sgn 7422  acdc2lem2 7431  acdc5lem2 7434  xpnnen 7441  xpomen 7442  znnen 7445  qnnen 7446  infpn2 7452  ruclem5 7457  ruclem13 7465  ruclem15 7467  ruclem17 7469  ruclem22 7474  ruclem23 7475  ruclem24 7476  ruclem25 7477  ruclem26 7478  ruclem27 7479  ruclem28 7480  ruclem29 7481  ruclem30 7482  ruclem31 7483  ruclem32 7484  ruclem33 7485  ruclem35 7487  ruclem39 7491  resdomq 7493  aleph1re 7494  infxpidmlem9 7503  infxpidmlem12 7506  infcda 7510  infdif 7511  infdif2 7512  infxp 7515  infmap1 7516  iunctb 7517  aleph1irr 7520  qdensere 7691  ismeti 7741  cnmetba 7842  cnmet 7843  cncfmet 7844  cncfmet1 7845  remetba 7848  tgioo 7854  dscmet 7856  lmbrf 7868  iscauf 7877  iscau5 7878  lmsslem 7887  caussi 7889  lmclimnn 7899  xpcn 7910  fsumcnlem 7923  bcth 7966  isgrpi 7976  grprn 7990  isgrp2i 8011  issubgi 8059  ghgrpilem4 8073  ghsubgi 8075  cnring 8099  ringsn 8100  vsfval 8194  nvcli 8228  cnnvnm 8250  nmcnilem 8272  abscn 8277  abscncfALT 8278  va1cnlem 8279  sm1cnilem 8281  ipid 8297  ipcl 8299  lnocoi 8352  nmlno0lem 8385  nmlno0i 8386  nmblolbi 8391  isblo3i 8392  blocni 8396  blocn 8398  ip0i 8415  ip1ilem 8416  ip2i 8418  ipdirilem 8419  ipasslem1 8421  ipasslem2 8422  ipasslem6 8426  ipasslem7 8427  ipasslem8 8428  ipasslem10 8430  ip2dii 8435  pythi 8441  siilem1 8442  siii 8444  ipblnfi 8447  ajfuni 8451  ubthi 8475  minveclem1 8476  minveclem3 8478  minveclem9 8484  minveclem10 8485  minveclem14 8489  minveclem19 8494  minveclem21 8496  minveclem25 8500  minveclem28 8503  minveclem29 8504  minvecex 8509  minveclem35 8510  minvecdist 8516  minveclem39 8518  htthlem12 8561  spwval2 8577  sincolem 8584  sincnlem 8585  sinco 8586  cosco 8587  pilem1 8590  pilem2 8591  pilem3 8592  pigt2lt4 8594  sinhalfpilem 8598  sincosq1lem 8620  sincosq1sgn 8621  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  sinq12gt0t 8625  sincos4thpi 8627  sincos6thpi 8628  cosh111lem1 8629  cosh111t 8632  efghgrpilem 8634  efif 8636  efifolem1 8637  efifolem2 8638  efifolem3 8639  efifolem4 8640  efifolem5 8641  efifolem6 8642  efifolem7 8643  efif1lem1 8645  efif1lem2 8646  efif1lem3 8647  efif1lem4 8648  efif1lem5 8649  efif1lem6 8650  efif1lem7 8651  circgrpOLD 8658  circgrp 8660  eff1i 8665  effoi 8666  effoiOLD 8667  resslogrn 8675  relogf1o 8679  log1 8688  loge 8689  pilog 8690  log1OLD 8707  logeOLD 8708  h2hcau 8788  h2hlm 8789  hvmulex 8802  hvmulcl 8805  hvaddcl 8809  hvcom 8810  hvsubval 8811  hvsubcl 8812  hvadd4 8846  hicl 8869  his1 8887  normlem6 8902  normlem7 8903  norm-ii 8925  normpyth 8930  hhip 8965  hhph 8966  bcsALT 8967  hlim0 9026  hlimcaui 9027  shsspwh 9039  hhssnm 9052  hhssabl 9053  hhssnv 9054  hhshsslem1 9057  hhshsslem2 9058  hhssvs 9061  hhssph 9063  occon2 9078  projlem2 9103  projlem3 9104  projlem4 9105  projlem5 9106  projlem6 9107  projlem8 9109  projlem13 9114  projlem14 9115  projlem15 9116  projlem18 9119  projlem28 9129  pjthlem1 9134  omlsilem 9159  pjpj0 9170  pjpjth 9174  pjop 9177  pjpo 9178  shsel 9195  shscl 9196  chjval 9238  shscom 9247  shsva 9248  shsel1 9249  shsel2 9250  shslej 9253  shjcom 9255  shjcl 9259  shlub 9261  shsumval2 9275  chsscon3 9299  chdmm1 9315  shjshs 9330  chabs1 9356  chabs2 9357  ledi 9374  span0 9380  spanun 9382  sshhococ 9384  chsup0 9386  h1de2 9391  spansnpj 9418  pjoml4 9447  cmbr 9450  fh1 9481  fh2 9482  nonbool 9513  5oa 9523  pjadd 9537  pjmul 9539  pjsslem 9541  pjdifnorm 9545  pjnel 9585  mayete3 9590  dfiop2 9596  hoeq 9604  hocof 9609  hoaddcl 9611  hosubcl 9612  honegsub 9639  hosubeq0 9669  ho01 9671  eigpos 9679  nmopsetn0 9709  nmfnsetn0 9722  hhlno 9743  hhnmo 9744  hhblo 9745  hh0o 9746  nmopneg 9805  0cnfn 9820  0lnfn 9825  nmop0 9826  nmfn0 9827  nmlnop0ALT 9835  lnopco0 9844  lnopeq0lem1 9845  lnopunilem2 9851  lnophmlem2 9857  nmcopexlem2 9867  lnopcon 9878  lnfn0 9886  nmcfnexlem2 9896  lnfncon 9905  nlelsh 9908  cnlnadjlem8 9922  cnlnadjlem9 9923  adjbd1o 9933  bdophs 9943  bdopco 9945  adjco 9947  nmopcoadj 9948  unierr 9950  idleop 9976  hmopidmpj 9991  pjssdif2 10013  pjssdif1 10014  pjima 10015  pjinvar 10029  pjcmmul1 10039  pjcmmul2 10040  stcltr1 10111  mdsl1 10156  mdslmd1 10164  mdsldmd1 10166  mdslmd3 10167  mdexch 10170  shatomistic 10196  hatomistic 10197  chpssat 10198  cvat 10201  cvbr3 10202  cvexchlem 10203  cvexch 10204  chrelat3 10207  mdsymlem6 10243  mdsym 10246  sumdmdi 10249  cmmd 10250  cmdmd 10251  sumdmd 10254  dmdbr6at 10256  mdcompl 10261  dmdcompl 10262  mddmdin0 10263  abs2sqle 10277  abs2sqlt 10278  abs2dif 10281  abs2difabs 10282  elghom 10289  ghomgrpilem1 10290  ghomgrpilem2 10291  ghomsn 10293  symgval 10308  symggrpiOLD 10311  symgidiOLD 10312  symggrpi 10313  symgidi 10314  cayleylem2 10317  cayleylem3 10318  mapdiscn 10398  homcard 10426  subsp 10429  iintlem2 10477  1alg 10498  eloi 10503  1ded 10515  0alg 10533  0ded 10534  0cat 10535  1cat 10536  mrdmcd 10566

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 147  df-an 225

Copyright terms: Public domain