MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant3 Unicode version

Theorem 3adant3 975
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3adant3  |-  ( (
ph  /\  ps  /\  th )  ->  ch )

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 952 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 15 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  vtoclgft  2834  eqeu  2936  disjprg  4019  ordelinel  4491  ordunel  4618  funopg  5286  fnco  5352  resasplit  5411  fresaunres2  5413  resdif  5494  fnimapr  5583  fsnunfv  5720  f1ocnvfvb  5795  soisores  5824  f1oiso2  5849  ovig  5969  ov6g  5985  ovg  5986  frxp  6225  poxp  6227  moriotass  6334  f1ofveu  6339  onfununi  6358  smores3  6370  smoiso  6379  smoord  6382  smogt  6384  oaord  6545  oaword  6547  omord2  6565  omcan  6567  omword  6568  omwordi  6569  oneo  6579  oeord  6586  oecan  6587  oeword  6588  oewordi  6589  nnaord  6617  nnaword  6625  nnmwordi  6633  omabslem  6644  nnneo  6649  erov  6755  ecopovtrn  6761  undifixp  6852  xpdom3  6960  mapxpen  7027  dif1enOLD  7090  dif1en  7091  fimax2g  7103  unbnn  7113  fipreima  7161  suppr  7219  unwdomg  7298  epfrs  7413  tskwe  7583  dif1card  7638  infxpenlem  7641  cdaun  7798  cdaenun  7800  ficardun  7828  infcdaabs  7832  infcda  7834  infdif2  7836  infxpdom  7837  ackbij1lem9  7854  ackbij1lem16  7861  cflim2  7889  cfslb  7892  cfsmolem  7896  coftr  7899  infpssrlem4  7932  isf34lem7  8005  hsmexlem2  8053  axcc2lem  8062  axdc3lem4  8079  axcclem  8083  winainflem  8315  tskssel  8379  tskpr  8392  tskop  8393  tskint  8407  tskxp  8409  tskmap  8410  gruop  8427  grothpw  8448  grothpwex  8449  grothomex  8451  adderpqlem  8578  mulerpqlem  8579  addassnq  8582  mulassnq  8583  mulcanenq  8584  distrnq  8585  ltsonq  8593  ltanq  8595  ltmnq  8596  genpass  8633  distrlem1pr  8649  distrlem5pr  8651  ltsopr  8656  reclem3pr  8673  ltasr  8722  axlttrn  8895  axltadd  8896  lelttr  8912  mul12  8978  add12  9025  subadd  9054  addsub  9062  npncan  9069  nppcan  9070  nppcan3  9071  pnpcan  9086  pnncan  9088  ppncan  9089  subdi  9213  ltaddsub2  9249  leaddsub2  9251  receu  9413  divass  9442  div23  9443  divcan4  9449  divsubdir  9456  divcan5  9462  divdiv32  9468  divdiv2  9472  div2sub  9585  letrp1  9598  lemul1  9608  ltmulgt12  9617  lediv1  9621  ltdiv2  9641  lediv2  9646  ltdiv23  9647  lediv23  9648  lbinfmle  9709  infmrcl  9733  rpnnen1lem5  10346  xrlelttr  10487  xrre2  10499  xrmaxlt  10510  xrmaxle  10512  qsqueeze  10528  xaddass  10569  xltadd1  10576  xmulasslem3  10606  xmulass  10607  xltmul1  10612  xadddir  10616  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  ixxdisj  10671  ixxub  10677  ixxlb  10678  ubioc1  10705  lbico1  10706  elioo5  10708  iccsupr  10736  lbicc2  10752  ubicc2  10753  iccneg  10757  icoshft  10758  icodisj  10761  snunico  10763  prunioo  10764  iccsplit  10768  iccf1o  10778  fzen  10811  fzrevral2  10867  fzshftral  10869  fzosubel2  10909  modmulnn  10988  modabs  10997  moddi  11007  modsubdir  11008  exprec  11143  expdiv  11152  expubnd  11162  sqdiv  11169  bernneq2  11228  bcval3  11319  bccmpl  11322  hashgadd  11359  hashun  11364  hashbclem  11390  ccatval1  11431  ccatval2  11432  ccatass  11436  ccatopth2  11463  ccatco  11490  shftval2  11570  mulre  11606  elicc4abs  11803  abssubge0  11811  abssuble0  11812  caubnd  11842  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  rpnnen2lem7  12499  dvdscmul  12555  dvdscmulr  12557  dvdsle  12574  dvdsleabs  12575  dvdsexp  12584  divalglem8  12599  divalgb  12603  sadass  12662  gcdass  12724  mulgcdr  12727  gcddiv  12728  qredeq  12785  qredeu  12786  euclemma  12787  prmdvdsexpb  12794  prmexpb  12796  coprimeprodsq  12862  coprimeprodsq2  12863  pythagtriplem1  12869  pythagtriplem3  12871  pythagtriplem6  12874  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  pythagtriplem19  12886  pythagtrip  12887  pcmul  12904  pcdiv  12905  pcqcl  12909  pcgcd1  12929  pcgcd  12930  pcfaclem  12946  ercpbl  13451  mreintcl  13497  ismred2  13505  mrcun  13524  submrc  13530  isfunc  13738  cofulid  13764  catcisolem  13938  posasymb  14086  isposi  14090  pleval2  14099  pltval3  14101  lubprop  14114  glbprop  14119  p0le  14149  latleeqm1  14185  lubss  14225  lubun  14227  clatglbss  14231  poslubdg  14252  mrelatglb0  14288  pslem  14315  spwpr4  14340  dirtr  14358  pwspjmhm  14444  gsumccat  14464  grpinvid1  14530  grpinvid2  14531  grpinvadd  14544  grpsubadd  14553  grppncan  14556  pwsinvg  14607  divssub  14677  odeq  14865  odf1o1  14883  odf1o2  14884  slwpss  14923  sylow2blem2  14932  lsmsubg  14965  lsmcom2  14966  lsmlub  14974  lsmss1  14975  lsmss2  14977  lsmass  14979  ablfaclem3  15322  mulgass2  15387  gsumdixp  15392  dvrcan1  15473  dvrcan3  15474  isabvd  15585  abvgt0  15593  abvres  15604  islss  15692  lspss  15741  lspssp  15745  lsslsp  15772  0lmhm  15797  reslmhm2b  15811  lsmcl  15836  lsmsp2  15840  lidlnegcl  15966  lidlnz  15980  aspss  16072  evlslem4  16245  coe1sclmul  16358  coe1sclmulfv  16359  coe1sclmul2  16360  xrsdsreclblem  16417  xrsdsreclb  16418  chrcong  16483  zndvds  16503  zntoslem  16510  ocvsscon  16575  basgen  16726  clsss  16791  ntrin  16798  elcls  16810  ntrcls0  16813  neiint  16841  neiss  16846  neips  16850  opnssneib  16852  innei  16862  islp2  16877  restco  16895  restcls  16911  restntr  16912  ordtopn3  16926  ordtcld3  16929  iscnp  16967  cnconst2  17011  t1ficld  17055  cmpsublem  17126  cmpcld  17129  clscon  17156  ptpjcn  17305  ptpjopn  17306  txcn  17320  ptrescn  17333  xkopjcn  17350  kqfeq  17415  kqfvima  17421  opnfbas  17537  filin  17549  neifil  17575  filuni  17580  cfinfil  17588  ufprim  17604  filufint  17615  ufinffr  17624  fin1aufil  17627  flimclslem  17679  flfneii  17687  fcfval  17728  alexsubALT  17745  cldsubg  17793  divstgphaus  17805  tsmsxp  17837  xmetlecl  17911  xmetsym  17912  prdsxmetlem  17932  xblcntr  17963  blssec  17981  blpnfctr  17982  txmetcn  18094  nmrpcl  18141  nm2dif  18146  nminvr  18180  nmoeq0  18245  0nmhm  18264  cnmet  18281  metds0  18354  metdscn2  18361  cnmpt2pc  18426  iihalf1  18429  iihalf2  18431  icchmeo  18439  bndth  18456  pi1xfr  18553  nmhmcn  18601  cphnmvs  18626  lmmbr2  18685  cfil3i  18695  bcthlem5  18750  resscdrg  18775  ovolfioo  18827  ovolficc  18828  ovolsscl  18845  ovolssnul  18846  ovoliunlem2  18862  volun  18902  iundisj2  18906  iunmbl2  18914  ovolioo  18925  itg2const  19095  cniccibl  19195  limcfval  19222  dvid  19267  dvnp1  19274  dvfsum2  19381  evlsval  19403  tdeglem3  19445  mdegmullem  19464  deg1scl  19499  deg1mul3le  19502  ig1pval3  19560  ig1pdvds  19562  ply1term  19586  coe1term  19640  dgradd2  19649  dvply1  19664  facth  19686  quotcan  19689  dvtaylp  19749  ptolemy  19864  sinq12gt0  19875  sincosq1eq  19880  efgh  19903  explog  19947  argrege0  19965  logimul  19968  angcan  20100  ang180lem2  20108  ang180lem3  20109  pythag  20115  logrec  20117  isosctrlem1  20118  isosctrlem2  20119  angpieqvd  20128  mumullem2  20418  lgsval4  20555  lgsmod  20560  padicabv  20779  grpoinvid1  20897  grpoinvid2  20898  grpoasscan1  20904  grpoasscan2  20905  grpoinvop  20908  grpopncan  20918  grponpcan  20919  grpopnpcan2  20920  gxcl  20932  gxinv  20937  gxinv2  20938  gxsuc  20939  gxid  20940  gxnn0add  20941  gxnn0mul  20944  ablonncan  20961  issubgoi  20977  ablomul  21022  vcsubdir  21112  vcnegsubdi2  21131  vcoprnelem  21134  isvc  21137  isnv  21168  nvscom  21187  nvmul0or  21210  nvpncan2  21214  nvaddsub4  21219  nvnncan  21221  nvdif  21231  nvpi  21232  nvabs  21239  nv1  21242  imsmetlem  21259  0oval  21366  lnon0  21376  blometi  21381  ajfval  21387  ipasslem5  21413  ajval  21440  hlipgt0  21493  ssphl  21496  hvadd12  21614  hvmulcom  21622  hvsubass  21623  hvsubdistr1  21628  hvsubdistr2  21629  hvaddcan2  21650  hvmulcan  21651  hvmulcan2  21652  hvsubcan  21653  hvsubcan2  21654  his7  21669  his2sub  21671  his2sub2  21672  bcs2  21761  bcs3  21762  hhssnv  21841  chj12  22113  spansncol  22147  cm2j  22199  homul12  22385  hoaddsub  22396  unopf1o  22496  adj2  22514  braadd  22525  kbmul  22535  eigvalcl  22541  lnopmulsubi  22556  hmopco  22603  cnlnadjlem2  22648  adjlnop  22666  leopmul  22714  leoptr  22717  hstoh  22812  strlem3a  22832  hstrlem3a  22840  cvntr  22872  dmdsl3  22895  atexch  22961  atcvatlem  22965  mdsymlem5  22987  cdj3lem2  23015  cdj3lem3  23018  ballotlemsgt1  23069  ballotlemrv1  23079  ballotlemrv2  23080  ballotlemfrcn0  23088  xreceu  23105  curry2ima  23247  iocinioc2  23272  iundisj2fi  23364  iundisj2f  23366  logeq0im1  23396  logccne0  23397  logccne0ALT  23398  logbid1  23400  logblt  23408  measres  23549  indfval  23600  cndprobtot  23639  cndprobprob  23641  iseupa  23881  ghomgsg  24000  ghomf1olem  24001  lediv2aALT  24013  mulcan1g  24084  mulsuble0b  24088  dvdspw  24103  fununiq  24126  trpredpo  24238  wfrlem3  24258  wfrlem4  24259  wfrlem9  24264  sltres  24318  nodenselem8  24342  nocvxmin  24345  nofulllem3  24358  nofulllem4  24359  brbtwn2  24533  axcgrid  24544  axsegconlem6  24550  axsegconlem7  24551  axsegconlem8  24552  axsegconlem9  24553  axsegconlem10  24554  ax5seglem1  24556  ax5seglem2  24557  axpasch  24569  axlowdimlem14  24583  axlowdimlem16  24585  axeuclidlem  24590  axcontlem2  24593  axcontlem5  24596  lineext  24699  linecgr  24704  lineelsb2  24771  bpolycl  24787  areacirclem4  24927  areacirclem5  24929  areacirclem6  24930  oprssopvg  25034  inttrp  25108  prl  25167  prjmapcp2  25170  valcurfn1  25204  isoriso2  25213  prltub  25260  ubpar  25261  supdef  25262  supaub  25273  supwlub  25274  fprod2  25330  reacomsmgrp2  25344  abloinvop  25353  grpodivone  25373  prsubrtr  25399  ltrooo  25404  rltrran  25414  multinvb  25423  zerdivemp1  25436  rngoridfz  25437  svli2  25484  svs2  25487  islp3  25514  hmeogrpi  25536  intcont  25543  cnfilca  25556  flfneih  25560  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs  25580  islimrs3  25581  islimrs4  25582  bwt2  25592  dmse1  25603  mslb1  25607  2wsms  25608  msra3  25609  nolimf2  25620  lvsovso  25626  supnuf  25629  addcanri  25666  negveud  25668  negveudr  25669  eqidob  25795  cmphmib  25799  cmpassoh  25801  cmpmon  25815  iepiclem  25823  vtare  25885  vtarsu  25886  vtarl  25887  tartarmap  25888  cmp2morp  25958  cmp2morpcats  25961  cmp2morpcatt  25962  cmppar3  25974  cmpmor  25975  setiscat  25979  indcls2  25996  clscnc  26010  clsun  26246  neiin  26250  ivthALT  26258  fness  26282  neifg  26320  eltail  26323  fimaxre2OLD  26431  fzmul  26443  lpss2  26468  heiborlem3  26537  exidreslem  26567  ghomco  26573  rngoneglmul  26582  zerdivemp1x  26586  isdrngo2  26589  rngogrphom  26602  smprngopr  26677  eldioph2  26841  elmapresaun  26850  dvdsrabdioph  26891  rabrenfdioph  26897  pellexlem5  26918  pellex  26920  pell14qrdivcl  26950  pell14qrgapw  26961  pellfund14gap  26972  reglogmul  26978  reglogexp  26979  monotoddzzfi  27027  monotoddzz  27028  zindbi  27031  jm2.17a  27047  jm2.17b  27048  congadd  27053  dvdsleabs2  27077  dvdsabsmod0  27079  jm2.19lem2  27083  jm2.19lem3  27084  jm2.19  27086  jm2.22  27088  jm2.23  27089  jm2.16nn0  27097  rmydioph  27107  rmxdiophlem  27108  jm3.1  27113  islssfgi  27170  pwssplit0  27187  pwssplit4  27191  uvcval  27234  uvcresum  27242  frlmsslsp  27248  f1lindf  27292  lnrfgtr  27324  hbtlem5  27332  pmtrval  27394  pmtrrn  27399  dvconstbi  27551  refsumcn  27701  fmuldfeq  27713  climsuselem1  27733  stoweidlem10  27759  stoweidlem14  27763  stoweidlem20  27769  stoweidlem28  27777  stoweidlem34  27783  stoweidlem51  27800  stoweidlem56  27805  stoweidlem59  27808  sigaraf  27843  sigarmf  27844  sigarls  27847  s2f1o  28091  frgra3v  28180  3vfriswmgra  28183  reccot  28228  rectan  28229  chordthmALT  28710  bnj553  28930  bnj966  28976  bnj967  28977  bnj1125  29022  bnj1173  29032  lubunNEW  29163  lsmsat  29198  lsmsatcv  29200  lcvexchlem4  29227  lcvexchlem5  29228  lfli  29251  lflcl  29254  lflmul  29258  lfl1  29260  eqlkr  29289  lshpkrlem4  29303  opcon3b  29386  oplecon3b  29390  oplecon1b  29391  opltcon3b  29394  opltcon1b  29395  oldmm1  29407  oldmm2  29408  oldmj1  29411  oldmj2  29412  olj01  29415  omllaw2N  29434  omllaw3  29435  cmtcomlemN  29438  omlfh1N  29448  omlfh3N  29449  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrcon3b  29467  cvrnbtwn4  29469  leatb  29482  atcmp  29501  atnlt  29503  atcvreq0  29504  atncvrN  29505  atnle  29507  atlatle  29510  cvlexchb1  29520  hlrelat5N  29590  atcvr0eq  29615  lnnat  29616  atexchltN  29630  3at  29679  llnnlt  29712  lplnnlt  29754  2llnjaN  29755  2llnjN  29756  2atnelvolN  29776  lvolnltN  29807  2lplnj  29809  dalem21  29883  dalem23  29885  dalem24  29886  dalem25  29887  dalem29  29890  dalem30  29891  dalem31N  29892  dalem32  29893  dalem33  29894  dalem34  29895  dalem35  29896  dalem36  29897  dalem37  29898  dalem40  29901  dalem46  29907  dalem47  29908  dalem58  29919  dalem59  29920  pmaple  29950  pmapglbx  29958  elpaddri  29991  paddclN  30031  pmapjoin  30041  pmapjat1  30042  pmapjat2  30043  pclun2N  30088  polcon3N  30106  2polcon4bN  30107  polcon2N  30108  paddunN  30116  poldmj1N  30117  pmapj2N  30118  pmapocjN  30119  psubclinN  30137  paddatclN  30138  poml5N  30143  osumcllem3N  30147  osumcllem4N  30148  osumcllem11N  30155  pl42lem4N  30171  lhpmcvr5N  30216  lhp2at0  30221  lhpelim  30226  lhple  30231  lautco  30286  ldilco  30305  ltrncl  30314  ltrn11  30315  ltrncnvnid  30316  ltrnle  30318  ltrncnvleN  30319  ltrnm  30320  ltrnj  30321  ltrncvr  30322  ltrnval1  30323  ltrncnvatb  30327  ltrncnvel  30331  ltrneq2  30337  trlval2  30352  trlcnv  30354  trljat1  30355  trlne  30374  cdleme8  30439  cdlemefrs29pre00  30584  cdleme42a  30660  cdlemeg49lebilem  30728  cdlemg7fvbwN  30796  ltrnco  30908  trljco  30929  trljco2  30930  tgrpov  30937  tendocl  30956  tendopl2  30966  diaord  31237  cdlemm10N  31308  dibord  31349  dicvaddcl  31380  dicvscacl  31381  dihvalcqpre  31425  dihord6apre  31446  dihord3  31447  dihord4  31448  dihmeetlem1N  31480  dihglblem3N  31485  dihmeetlem2N  31489  dihlspsnssN  31522  dihlspsnat  31523  dihglblem6  31530  dochss  31555  dochshpncl  31574  dochdmj1  31580  dochkr1  31668  dochkr1OLDN  31669  lcfl6  31690  lcfrlem16  31748  hgmapval0  32085  hgmapvvlem3  32118  hdmapglem7  32122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator