Theorem mp2an 694

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  2false 716  mp3an 912  vtocl2 1818  cla4e2v 1843  mosub 1894  sbccomg 1960  csbex 1980  sseq12i 2058  uneq12i 2153  ineq12i 2186  keephyp 2367  opeq12i 2461  breq12i 2596  opthwiener 2770  opelopab 2782  brab 2783  ideq 2801  onssel 3072  onun 3073  onsucss 3074  tfis 3090  finds 3119  finds2 3121  onnev 3204  eqrelriv 3213  xpex 3222  opelcnv 3255  brcnv 3256  intirr 3390  ssrnres 3427  cores 3441  coexg 3465  coex 3466  opabex 3549  fcoi1 3584  fcoi2 3585  fcnvres 3587  fabex 3593  fvopabf 3728  fopabcos 3772  fopabsn 3779  fvi 3781  fvresex 3796  abrexexlem2 3798  iunex 3802  tz7.44-2 3868  tz7.44-3 3869  tz7.48-2 3896  oprabss 3945  oprabex 3958  oprabex2 3960  1st2val 4033  2nd2val 4034  2ndconst 4035  df1st2 4064  df2nd2 4065  oawordeulem 4126  nneob 4193  ecoprcom 4257  ecoprass 4258  ecoprdi 4259  fnmap 4267  mapval 4270  elmap 4272  elpm 4274  entr 4351  endisj 4371  xpen 4420  pwen 4435  0sdom1dom 4456  unfilem1 4476  prfi 4483  fodomfi 4492  pwfi 4497  pm54.43 4498  en2lp 4526  inf0 4530  axinf2 4548  dfom3 4554  oancom 4557  infensuc 4562  trcl 4569  rankr1 4598  rankel 4604  rankss 4612  rankpr 4616  rankval4 4626  rankxplim 4636  rankxplim3 4638  scottex 4640  aceq3lem 4656  ac6lem 4678  numthlem 4707  zorn2lem1 4712  zorn2lem4 4715  cardon 4751  cardid 4752  carden 4755  cardsn 4757  carddom 4759  cardsdom 4760  domtri 4761  unxpdomlem 4766  unxpdom2 4768  sucxpdom 4769  cardprc 4784  alephsucpw 4793  aleph1 4794  alephord 4798  alephord3 4801  alephgeom 4805  alephfplem1 4819  alephfplem4 4822  alephfp2 4824  alephval2 4825  dominf 4827  cfom 4839  cdaval 4843  uncdadom 4844  pm110.643 4846  cdaen 4847  cda1en 4849  cdacomen 4852  cdaassen 4853  xpcdaen 4854  mapcdaen 4855  cdadom1 4856  cdadom3 4858  cdainf 4860  1lt2pi 4955  1q 4980  1lt2pq 5001  halfpq 5005  distrlem5pr 5054  0r 5112  1r 5113  m1r 5114  m1p1sr 5124  m1m1sr 5125  0lt1sr 5127  1ne0sr 5128  1idsr 5130  recexsrlem 5135  mappsrpr 5141  axresscn 5191  axi2m1 5208  addex 5240  mulex 5241  addcl 5243  mulcl 5244  addcom 5245  mulcom 5246  readdcl 5257  remulcl 5258  add4 5265  subcl 5289  subadd 5294  pncan3 5301  subneg 5327  subeq0 5328  mul4 5348  muladd 5349  resubcl 5362  addsub4 5397  xrltnrt 5465  mnfltpnf 5468  lttri2 5496  lttri3 5497  letri3 5498  leloe 5499  ltlen 5500  ltnsym 5501  lenlt 5502  ltle 5504  ltneOLD 5508  addgt0i 5526  mulgt0 5531  mulgt0i 5533  ltaddpos 5588  posdif 5589  ltnegcon1 5590  lenegcon1 5591  subge0 5600  recex 5609  muln0 5619  mulnzcnopr 5622  divval 5624  div0 5678  divmuldiv 5693  divadddiv 5695  divdivdiv 5696  redivcl 5705  recgt0i 5721  ltdiv23i 5794  nnssre 5826  nnind 5836  0nnn 5847  2nn 5897  3nn 5898  4nn 5900  8th4div3 5929  halfpm6th 5930  xrsupsslem 5974  xrinfmsslem 5975  xrsup0 5995  nn0addcl 6019  nn0mulcl 6020  nn0addge1 6030  nn0addge2 6031  halfnz 6092  dfuz 6101  uzindOLD 6107  om2uzran 6188  uzrdgini 6191  uzrdgfnuz 6194  seq1val 6200  seq1res 6215  ser1cl1 6218  ser1recl 6219  ser1ref 6220  ser1mono 6225  ser1add2 6226  ser1add 6227  shftidt 6243  seq1shftid 6244  ioomax 6276  ioopos 6277  icoshftf1oi 6293  icounlem 6296  snunioolem 6298  eluzaddi 6319  eluzsubi 6320  uzinfm 6345  fzshftralt 6405  seq0fval 6418  seqzfval 6420  seqzfn 6422  seq1seqz 6424  seq1seq0t 6427  seq1seq0 6428  seq0fn 6429  seq00 6433  serzcl1 6445  dfseq0 6446  ser0cl1 6447  ser0f 6448  sqmul 6498  sumsqne0 6516  cu2 6522  subsq 6528  nnsqcl 6541  nn0le2msqt 6544  nn0opthlem1 6545  nn0opth 6547  sqr0 6553  sqrlem1 6554  sqrlem2 6555  sqrlem6 6559  sqrlem8 6561  sqrlem13 6566  sqrlem24 6577  sqrgt0i 6578  sqrlem26 6579  sqrmuli 6585  sqr4 6598  sqr9 6599  sqr2gt1lt2 6600  sqr2irrlem1 6605  sqr2irrlem4 6608  i3 6614  nthruc 6627  nthruz 6628  crre 6657  crreOLD 6658  crim 6659  crimOLD 6660  cjmulge0 6679  abs00 6728  sqabsadd 6736  sqabssub 6737  abstri 6780  seq1bnd 6798  seq1ublem 6799  seq1ub 6800  ser1absdiflem 6817  fac1 6823  facp1t 6824  faclbnd4lem1 6836  bcpasc2 6856  bcpasc 6858  sumeq2 6874  fsump1s 6902  csbfsumlem 6915  fsumrev 6918  fsumshft 6920  serzref 6940  serzmulc 6947  ser0mulc 6948  ser1mulc 6949  binomlem6 6960  binom 6961  climunii 6986  climshft2 6994  climuz0 6996  climaddc 7019  climmulc 7020  iserzshft 7031  clim2serz 7032  climserzle 7034  climabslem 7035  climubi 7040  climsup 7042  climcau 7043  caucvglem2 7045  caucvg 7050  caucvg3a 7051  caucvg2 7052  caucvg3lem 7053  caucvg3t 7055  serzf0 7056  ser1f0 7057  ser1clim0 7060  ser1cmp 7061  ser1cmp0 7062  ser1cmp2 7064  iserzabslem 7065  cvgcmp2lem 7067  cvgcmp2clem 7069  cvgcmpub 7072  cvgcmp3c 7073  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  isumshft 7090  isumshft2 7091  isumsplit 7102  isum0split 7103  infcvgaux1 7105  infcvglem2 7108  fnsmnt 7112  expcnvlem1 7113  expcnvlem2 7114  expcnvlem4 7116  geoser 7120  geolimilem 7121  geolim1i 7124  georeclim 7126  0.999... 7132  cvgratlem1ALT 7133  cvgratlem2ALT 7134  fsum0diag 7144  fsum0diag2 7145  negfcncf 7155  abscncflem 7160  ivthlem1 7167  ivthlem4 7170  ivthlem5 7171  ivthlem6 7172  ivthlem7 7173  ivthlem8 7174  ivthlem9 7175  isupivth 7176  ivthlem4OLD 7179  ivthlem5OLD 7180  ivthlem6OLD 7181  ivthlem7OLD 7182  ivthlem8OLD 7183  ivthOLD 7184  ivth2OLD 7185  efcltlem1 7197  dfef2 7200  erelem6 7217  efcj 7229  efaddlem3 7233  efaddlem6 7236  efaddlem7 7237  efaddlem8 7238  efaddlem10 7240  efaddlem12 7242  efaddlem13 7243  efaddlem16 7246  efaddlem17 7247  efaddlem18 7248  efaddlem19 7249  efaddlem20 7250  efaddlem21 7251  efaddlem22 7252  efaddlem25 7255  efaddlem26 7256  efaddlem27 7257  ef1tllem 7274  ef01tllem1 7276  ef01tllem2 7277  ef01tlub 7278  absef01tllem 7279  absef01tlub 7280  eirrlem1 7281  eirrlem2 7282  eirrlem3 7283  eirrlem4 7284  eirrlem5 7285  abspef01tlub 7287  efsep 7288  efgt0 7296  eflt 7298  eflegeolem2 7305  efm1legeo 7308  efcnlem1 7310  efcn 7314  reeff1olem1 7315  reeff1olem1OLD 7317  sinadd 7344  cosadd 7345  sin01bndlem1 7360  sin01bndlem2 7361  sin01bndlem3 7362  cos01bndlem2 7363  cos01bndlem3 7364  cos1bnd 7367  cos2bnd 7368  sin01gt0 7369  cos01gt0 7370  sin02gt0 7371  sincos1sgn 7372  sincos2sgn 7373  acdc2lem2 7382  acdc5lem2 7385  xpnnen 7392  xpomen 7393  znnen 7396  qnnen 7397  infpn2 7403  ruclem5 7408  ruclem13 7416  ruclem15 7418  ruclem17 7420  ruclem22 7425  ruclem23 7426  ruclem24 7427  ruclem25 7428  ruclem26 7429  ruclem27 7430  ruclem28 7431  ruclem29 7432  ruclem30 7433  ruclem31 7434  ruclem32 7435  ruclem33 7436  ruclem35 7438  ruclem39 7442  resdomq 7444  aleph1re 7445  infxpidmlem9 7454  infxpidmlem12 7457  infcda 7461  infdif 7462  infdif2 7463  infxp 7466  infmap1 7467  iunctb 7468  aleph1irr 7471  qdensere 7639  ismeti 7689  cnmetba 7790  cnmet 7791  cncfmet 7792  cncfmet1 7793  remetba 7796  tgioo 7802  dscmet 7804  lmbrf 7816  iscauf 7825  iscau5 7826  lmsslem 7835  caussi 7837  lmclimnn 7847  xpcn 7858  fsumcnlem 7871  bcth 7914  isgrpi 7924  grprn 7938  isgrp2i 7959  issubgi 8007  ghgrpilem4 8021  ghsubgi 8023  cnring 8047  ringsn 8048  isvci 8053  isnvi 8110  vsfval 8132  nvcli 8165  cnnvnm 8187  nmcnilem 8209  va1cnlem 8214  sm1cnilem 8216  ipid 8232  ipcl 8234  lnocoi 8287  nmlno0lem 8320  nmlno0i 8321  nmblolbi 8326  isblo3i 8327  blocni 8331  blocn 8333  ip0i 8350  ip1ilem 8351  ip2i 8353  ipdirilem 8354  ipasslem1 8356  ipasslem2 8357  ipasslem6 8361  ipasslem7 8362  ipasslem8 8363  ipasslem10 8365  ip2dii 8370  pythi 8376  siilem1 8377  siii 8379  ipblnfi 8382  ajfuni 8386  ubthi 8410  minveclem1 8411  minveclem3 8413  minveclem9 8419  minveclem10 8420  minveclem14 8424  minveclem19 8429  minveclem21 8431  minveclem25 8435  minveclem28 8438  minveclem29 8439  minvecex 8444  minveclem35 8445  minvecdist 8451  minveclem39 8453  htthlem12 8495  sincolem 8497  sincnlem 8498  sinco 8499  cosco 8500  pilem1 8503  pilem2 8504  pilem3 8505  pigt2lt4 8507  sinhalfpilem 8511  sincosq1lem 8533  sincosq1sgn 8534  sincosq2sgn 8535  sincosq3sgn 8536  sincosq4sgn 8537  sinq12gt0t 8538  sincos4thpi 8540  sincos6thpi 8541  cosh111lem1 8542  cosh111t 8545  efghgrpilem 8547  efif 8549  efifolem1 8550  efifolem2 8551  efifolem3 8552  efifolem4 8553  efifolem5 8554  efifolem6 8555  efifolem7 8556  efif1lem1 8558  efif1lem2 8559  efif1lem3 8560  efif1lem4 8561  efif1lem5 8562  efif1lem6 8563  efif1lem7 8564  circgrpOLD 8571  circgrp 8573  eff1i 8578  effoi 8579  effoiOLD 8580  resslogrn 8588  relogf1o 8592  log1 8601  loge 8602  pilog 8603  log1OLD 8620  logeOLD 8621  abs2sqle 8639  abs2sqlt 8640  abs2dif 8643  abs2difabs 8644  elghom 8651  ghomgrpilem1 8652  ghomgrpilem2 8653  ghomsn 8655  symgval 8670  symggrpi 8673  symgidi 8674  cayleylem2 8677  cayleylem3 8678  subsp 8779  iintlem2 8827  1alg 8848  eloi 8853  1ded 8865  0alg 8883  0ded 8884  0cat 8885  1cat 8886  mrdmcd 8916  hvmulex 9029  hvmulcl 9032  hvaddcl 9037  hvcom 9038  hvsubval 9039  hvsubcl 9040  hvadd4 9074  hicl 9097  his1 9115  normlem6 9130  normlem7 9131  norm-ii 9153  normpyth 9158  hhsm 9185  hhnm 9187  hhip 9193  hhph 9194  bcsALT 9195  hillim 9216  hilcau 9217  hlim0 9256  hlimcaui 9257  shsspwh 9269  hhssnm 9282  occon2 9292  projlem2 9317  projlem3 9318  projlem4 9319  projlem5 9320  projlem6 9321  projlem8 9323  projlem13 9328  projlem14 9329  projlem15 9330  projlem18 9333  projlem28 9343  pjthlem1 9348  omlsilem 9373  pjpj0 9384  pjpjth 9388  pjop 9391  pjpo 9392  shsel 9409  shscl 9410  chjval 9452  shscom 9461  shsva 9462  shsel1 9463  shsel2 9464  shslej 9467  shjcom 9469  shjcl 9473  shlub 9475  shsumval2 9489  chsscon3 9513  chdmm1 9529  shjshs 9544  chabs1 9570  chabs2 9571  ledi 9588  span0 9594  spanun 9596  sshhococ 9598  chsup0 9600  h1de2 9605  spansnpj 9632  pjoml4 9661  cmbr 9664  fh1 9695  fh2 9696  nonbool 9727  5oa 9737  pjadd 9751  pjmul 9753  pjsslem 9755  pjdifnorm 9759  pjnel 9799  mayete3 9804  dfiop2 9810  hoeq 9818  hocof 9823  hoaddcl 9825  hosubcl 9826  honegsub 9853  hosubeq0 9883  ho01 9885  eigpos 9893  nmopsetn0 9923  nmfnsetn0 9936  hhlno 9957  hhnmo 9958  hhblo 9959  hh0o 9960  nmopneg 10019  0cnfn 10034  0lnfn 10039  nmop0 10040  nmfn0 10041  nmlnop0ALT 10049  lnopco0 10058  lnopeq0lem1 10059  lnopunilem2 10065  lnophmlem2 10071  nmcopexlem2 10081  lnopcon 10092  lnfn0 10100  nmcfnexlem2 10110  lnfncon 10119  nlelsh 10122  cnlnadjlem8 10136  cnlnadjlem9 10137  adjbd1o 10147  bdophs 10157  bdopco 10159  adjco 10161  nmopcoadj 10162  unierr 10164  idleop 10190  hmopidmpj 10205  pjssdif2 10227  pjssdif1 10228  pjima 10229  pjinvar 10243  pjcmmul1 10253  pjcmmul2 10254  stcltr1 10325  mdsl1 10370  mdslmd1 10378  mdsldmd1 10380  mdslmd3 10381  mdexch 10384  shatomistic 10410  hatomistic 10411  chpssat 10412  cvat 10415  cvbr3 10416  cvexchlem 10417  cvexch 10418  chrelat3 10421  mdsymlem6 10457  mdsym 10460  sumdmdi 10463  cmmd 10464  cmdmd 10465  sumdmd 10468  dmdbr6at 10470  mdcompl 10475  dmdcompl 10476  mddmdin0 10477

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