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  2836  eqeu  2938  disjprg  4021  ordelinel  4493  ordunel  4620  funopg  5288  fnco  5354  resasplit  5413  fresaunres2  5415  resdif  5496  fnimapr  5585  fsnunfv  5722  f1ocnvfvb  5797  soisores  5826  f1oiso2  5851  ovig  5971  ov6g  5987  ovg  5988  frxp  6227  poxp  6229  moriotass  6336  f1ofveu  6341  onfununi  6360  smores3  6372  smoiso  6381  smoord  6384  smogt  6386  oaord  6547  oaword  6549  omord2  6567  omcan  6569  omword  6570  omwordi  6571  oneo  6581  oeord  6588  oecan  6589  oeword  6590  oewordi  6591  nnaord  6619  nnaword  6627  nnmwordi  6635  omabslem  6646  nnneo  6651  erov  6757  ecopovtrn  6763  undifixp  6854  xpdom3  6962  mapxpen  7029  dif1enOLD  7092  dif1en  7093  fimax2g  7105  unbnn  7115  fipreima  7163  suppr  7221  unwdomg  7300  epfrs  7415  tskwe  7585  dif1card  7640  infxpenlem  7643  cdaun  7800  cdaenun  7802  ficardun  7830  infcdaabs  7834  infcda  7836  infdif2  7838  infxpdom  7839  ackbij1lem9  7856  ackbij1lem16  7863  cflim2  7891  cfslb  7894  cfsmolem  7898  coftr  7901  infpssrlem4  7934  isf34lem7  8007  hsmexlem2  8055  axcc2lem  8064  axdc3lem4  8081  axcclem  8085  winainflem  8317  tskssel  8381  tskpr  8394  tskop  8395  tskint  8409  tskxp  8411  tskmap  8412  gruop  8429  grothpw  8450  grothpwex  8451  grothomex  8453  adderpqlem  8580  mulerpqlem  8581  addassnq  8584  mulassnq  8585  mulcanenq  8586  distrnq  8587  ltsonq  8595  ltanq  8597  ltmnq  8598  genpass  8635  distrlem1pr  8651  distrlem5pr  8653  ltsopr  8658  reclem3pr  8675  ltasr  8724  axlttrn  8897  axltadd  8898  lelttr  8914  mul12  8980  add12  9027  subadd  9056  addsub  9064  npncan  9071  nppcan  9072  nppcan3  9073  pnpcan  9088  pnncan  9090  ppncan  9091  subdi  9215  ltaddsub2  9251  leaddsub2  9253  receu  9415  divass  9444  div23  9445  divcan4  9451  divsubdir  9458  divcan5  9464  divdiv32  9470  divdiv2  9474  div2sub  9587  letrp1  9600  lemul1  9610  ltmulgt12  9619  lediv1  9623  ltdiv2  9643  lediv2  9648  ltdiv23  9649  lediv23  9650  lbinfmle  9711  infmrcl  9735  rpnnen1lem5  10348  xrlelttr  10489  xrre2  10501  xrmaxlt  10512  xrmaxle  10514  qsqueeze  10530  xaddass  10571  xltadd1  10578  xmulasslem3  10608  xmulass  10609  xltmul1  10614  xadddir  10618  xrsupsslem  10627  xrinfmsslem  10628  supxrun  10636  ixxdisj  10673  ixxub  10679  ixxlb  10680  ubioc1  10707  lbico1  10708  elioo5  10710  iccsupr  10738  lbicc2  10754  ubicc2  10755  iccneg  10759  icoshft  10760  icodisj  10763  snunico  10765  prunioo  10766  iccsplit  10770  iccf1o  10780  fzen  10813  fzrevral2  10869  fzshftral  10871  fzosubel2  10911  modmulnn  10990  modabs  10999  moddi  11009  modsubdir  11010  exprec  11145  expdiv  11154  expubnd  11164  sqdiv  11171  bernneq2  11230  bcval3  11321  bccmpl  11324  hashgadd  11361  hashun  11366  hashbclem  11392  ccatval1  11433  ccatval2  11434  ccatass  11438  ccatopth2  11465  ccatco  11492  shftval2  11572  mulre  11608  elicc4abs  11805  abssubge0  11813  abssuble0  11814  caubnd  11844  sin01gt0  12472  cos01gt0  12473  sin02gt0  12474  rpnnen2lem7  12501  dvdscmul  12557  dvdscmulr  12559  dvdsle  12576  dvdsleabs  12577  dvdsexp  12586  divalglem8  12601  divalgb  12605  sadass  12664  gcdass  12726  mulgcdr  12729  gcddiv  12730  qredeq  12787  qredeu  12788  euclemma  12789  prmdvdsexpb  12796  prmexpb  12798  coprimeprodsq  12864  coprimeprodsq2  12865  pythagtriplem1  12871  pythagtriplem3  12873  pythagtriplem6  12876  pythagtriplem12  12881  pythagtriplem13  12882  pythagtriplem14  12883  pythagtriplem16  12885  pythagtriplem19  12888  pythagtrip  12889  pcmul  12906  pcdiv  12907  pcqcl  12911  pcgcd1  12931  pcgcd  12932  pcfaclem  12948  ercpbl  13453  mreintcl  13499  ismred2  13507  mrcun  13526  submrc  13532  isfunc  13740  cofulid  13766  catcisolem  13940  posasymb  14088  isposi  14092  pleval2  14101  pltval3  14103  lubprop  14116  glbprop  14121  p0le  14151  latleeqm1  14187  lubss  14227  lubun  14229  clatglbss  14233  poslubdg  14254  mrelatglb0  14290  pslem  14317  spwpr4  14342  dirtr  14360  pwspjmhm  14446  gsumccat  14466  grpinvid1  14532  grpinvid2  14533  grpinvadd  14546  grpsubadd  14555  grppncan  14558  pwsinvg  14609  divssub  14679  odeq  14867  odf1o1  14885  odf1o2  14886  slwpss  14925  sylow2blem2  14934  lsmsubg  14967  lsmcom2  14968  lsmlub  14976  lsmss1  14977  lsmss2  14979  lsmass  14981  ablfaclem3  15324  mulgass2  15389  gsumdixp  15394  dvrcan1  15475  dvrcan3  15476  isabvd  15587  abvgt0  15595  abvres  15606  islss  15694  lspss  15743  lspssp  15747  lsslsp  15774  0lmhm  15799  reslmhm2b  15813  lsmcl  15838  lsmsp2  15842  lidlnegcl  15968  lidlnz  15982  aspss  16074  evlslem4  16247  coe1sclmul  16360  coe1sclmulfv  16361  coe1sclmul2  16362  xrsdsreclblem  16419  xrsdsreclb  16420  chrcong  16485  zndvds  16505  zntoslem  16512  ocvsscon  16577  basgen  16728  clsss  16793  ntrin  16800  elcls  16812  ntrcls0  16815  neiint  16843  neiss  16848  neips  16852  opnssneib  16854  innei  16864  islp2  16879  restco  16897  restcls  16913  restntr  16914  ordtopn3  16928  ordtcld3  16931  iscnp  16969  cnconst2  17013  t1ficld  17057  cmpsublem  17128  cmpcld  17131  clscon  17158  ptpjcn  17307  ptpjopn  17308  txcn  17322  ptrescn  17335  xkopjcn  17352  kqfeq  17417  kqfvima  17423  opnfbas  17539  filin  17551  neifil  17577  filuni  17582  cfinfil  17590  ufprim  17606  filufint  17617  ufinffr  17626  fin1aufil  17629  flimclslem  17681  flfneii  17689  fcfval  17730  alexsubALT  17747  cldsubg  17795  divstgphaus  17807  tsmsxp  17839  xmetlecl  17913  xmetsym  17914  prdsxmetlem  17934  xblcntr  17965  blssec  17983  blpnfctr  17984  txmetcn  18096  nmrpcl  18143  nm2dif  18148  nminvr  18182  nmoeq0  18247  0nmhm  18266  cnmet  18283  metds0  18356  metdscn2  18363  cnmpt2pc  18428  iihalf1  18431  iihalf2  18433  icchmeo  18441  bndth  18458  pi1xfr  18555  nmhmcn  18603  cphnmvs  18628  lmmbr2  18687  cfil3i  18697  bcthlem5  18752  resscdrg  18777  ovolfioo  18829  ovolficc  18830  ovolsscl  18847  ovolssnul  18848  ovoliunlem2  18864  volun  18904  iundisj2  18908  iunmbl2  18916  ovolioo  18927  itg2const  19097  cniccibl  19197  limcfval  19224  dvid  19269  dvnp1  19276  dvfsum2  19383  evlsval  19405  tdeglem3  19447  mdegmullem  19466  deg1scl  19501  deg1mul3le  19504  ig1pval3  19562  ig1pdvds  19564  ply1term  19588  coe1term  19642  dgradd2  19651  dvply1  19666  facth  19688  quotcan  19691  dvtaylp  19751  ptolemy  19866  sinq12gt0  19877  sincosq1eq  19882  efgh  19905  explog  19949  argrege0  19967  logimul  19970  angcan  20102  ang180lem2  20110  ang180lem3  20111  pythag  20117  logrec  20119  isosctrlem1  20120  isosctrlem2  20121  angpieqvd  20130  mumullem2  20420  lgsval4  20557  lgsmod  20562  padicabv  20781  grpoinvid1  20899  grpoinvid2  20900  grpoasscan1  20906  grpoasscan2  20907  grpoinvop  20910  grpopncan  20920  grponpcan  20921  grpopnpcan2  20922  gxcl  20934  gxinv  20939  gxinv2  20940  gxsuc  20941  gxid  20942  gxnn0add  20943  gxnn0mul  20946  ablonncan  20963  issubgoi  20979  ablomul  21024  vcsubdir  21114  vcnegsubdi2  21133  vcoprnelem  21136  isvc  21139  isnv  21170  nvscom  21189  nvmul0or  21212  nvpncan2  21216  nvaddsub4  21221  nvnncan  21223  nvdif  21233  nvpi  21234  nvabs  21241  nv1  21244  imsmetlem  21261  0oval  21368  lnon0  21378  blometi  21383  ajfval  21389  ipasslem5  21415  ajval  21442  hlipgt0  21495  ssphl  21498  hvadd12  21616  hvmulcom  21624  hvsubass  21625  hvsubdistr1  21630  hvsubdistr2  21631  hvaddcan2  21652  hvmulcan  21653  hvmulcan2  21654  hvsubcan  21655  hvsubcan2  21656  his7  21671  his2sub  21673  his2sub2  21674  bcs2  21763  bcs3  21764  hhssnv  21843  chj12  22115  spansncol  22149  cm2j  22201  homul12  22387  hoaddsub  22398  unopf1o  22498  adj2  22516  braadd  22527  kbmul  22537  eigvalcl  22543  lnopmulsubi  22558  hmopco  22605  cnlnadjlem2  22650  adjlnop  22668  leopmul  22716  leoptr  22719  hstoh  22814  strlem3a  22834  hstrlem3a  22842  cvntr  22874  dmdsl3  22897  atexch  22963  atcvatlem  22967  mdsymlem5  22989  cdj3lem2  23017  cdj3lem3  23020  ballotlemsgt1  23071  ballotlemrv1  23081  ballotlemrv2  23082  ballotlemfrcn0  23090  xreceu  23107  curry2ima  23249  iocinioc2  23274  iundisj2fi  23366  iundisj2f  23368  logeq0im1  23398  logccne0  23399  logccne0ALT  23400  logbid1  23402  logblt  23410  measres  23551  indfval  23602  cndprobtot  23641  cndprobprob  23643  iseupa  23883  ghomgsg  24002  ghomf1olem  24003  lediv2aALT  24015  mulcan1g  24086  mulsuble0b  24090  dvdspw  24105  fununiq  24128  trpredpo  24240  wfrlem3  24260  wfrlem4  24261  wfrlem9  24266  sltres  24320  nodenselem8  24344  nocvxmin  24347  nofulllem3  24360  nofulllem4  24361  brbtwn2  24535  axcgrid  24546  axsegconlem6  24552  axsegconlem7  24553  axsegconlem8  24554  axsegconlem9  24555  axsegconlem10  24556  ax5seglem1  24558  ax5seglem2  24559  axpasch  24571  axlowdimlem14  24585  axlowdimlem16  24587  axeuclidlem  24592  axcontlem2  24595  axcontlem5  24598  lineext  24701  linecgr  24706  lineelsb2  24773  bpolycl  24789  itg2addnc  24935  areacirclem4  24938  areacirclem5  24940  areacirclem6  24941  oprssopvg  25045  inttrp  25119  prl  25178  prjmapcp2  25181  valcurfn1  25215  isoriso2  25224  prltub  25271  ubpar  25272  supdef  25273  supaub  25284  supwlub  25285  fprod2  25341  reacomsmgrp2  25355  abloinvop  25364  grpodivone  25384  prsubrtr  25410  ltrooo  25415  rltrran  25425  multinvb  25434  zerdivemp1  25447  rngoridfz  25448  svli2  25495  svs2  25498  islp3  25525  hmeogrpi  25547  intcont  25554  cnfilca  25567  flfneih  25571  limptlimpr2lem1  25585  limptlimpr2lem2  25586  islimrs  25591  islimrs3  25592  islimrs4  25593  bwt2  25603  dmse1  25614  mslb1  25618  2wsms  25619  msra3  25620  nolimf2  25631  lvsovso  25637  supnuf  25640  addcanri  25677  negveud  25679  negveudr  25680  eqidob  25806  cmphmib  25810  cmpassoh  25812  cmpmon  25826  iepiclem  25834  vtare  25896  vtarsu  25897  vtarl  25898  tartarmap  25899  cmp2morp  25969  cmp2morpcats  25972  cmp2morpcatt  25973  cmppar3  25985  cmpmor  25986  setiscat  25990  indcls2  26007  clscnc  26021  clsun  26257  neiin  26261  ivthALT  26269  fness  26293  neifg  26331  eltail  26334  fimaxre2OLD  26442  fzmul  26454  lpss2  26479  heiborlem3  26548  exidreslem  26578  ghomco  26584  rngoneglmul  26593  zerdivemp1x  26597  isdrngo2  26600  rngogrphom  26613  smprngopr  26688  eldioph2  26852  elmapresaun  26861  dvdsrabdioph  26902  rabrenfdioph  26908  pellexlem5  26929  pellex  26931  pell14qrdivcl  26961  pell14qrgapw  26972  pellfund14gap  26983  reglogmul  26989  reglogexp  26990  monotoddzzfi  27038  monotoddzz  27039  zindbi  27042  jm2.17a  27058  jm2.17b  27059  congadd  27064  dvdsleabs2  27088  dvdsabsmod0  27090  jm2.19lem2  27094  jm2.19lem3  27095  jm2.19  27097  jm2.22  27099  jm2.23  27100  jm2.16nn0  27108  rmydioph  27118  rmxdiophlem  27119  jm3.1  27124  islssfgi  27181  pwssplit0  27198  pwssplit4  27202  uvcval  27245  uvcresum  27253  frlmsslsp  27259  f1lindf  27303  lnrfgtr  27335  hbtlem5  27343  pmtrval  27405  pmtrrn  27410  dvconstbi  27562  refsumcn  27712  fmuldfeq  27724  climsuselem1  27744  stoweidlem10  27770  stoweidlem14  27774  stoweidlem20  27780  stoweidlem28  27788  stoweidlem34  27794  stoweidlem51  27811  stoweidlem56  27816  stoweidlem59  27819  sigaraf  27854  sigarmf  27855  sigarls  27858  s2f1o  28102  frgra3v  28191  3vfriswmgra  28194  reccot  28239  rectan  28240  chordthmALT  28783  bnj553  29003  bnj966  29049  bnj967  29050  bnj1125  29095  bnj1173  29105  lubunNEW  29236  lsmsat  29271  lsmsatcv  29273  lcvexchlem4  29300  lcvexchlem5  29301  lfli  29324  lflcl  29327  lflmul  29331  lfl1  29333  eqlkr  29362  lshpkrlem4  29376  opcon3b  29459  oplecon3b  29463  oplecon1b  29464  opltcon3b  29467  opltcon1b  29468  oldmm1  29480  oldmm2  29481  oldmj1  29484  oldmj2  29485  olj01  29488  omllaw2N  29507  omllaw3  29508  cmtcomlemN  29511  omlfh1N  29521  omlfh3N  29522  cvrnbtwn2  29538  cvrnbtwn3  29539  cvrcon3b  29540  cvrnbtwn4  29542  leatb  29555  atcmp  29574  atnlt  29576  atcvreq0  29577  atncvrN  29578  atnle  29580  atlatle  29583  cvlexchb1  29593  hlrelat5N  29663  atcvr0eq  29688  lnnat  29689  atexchltN  29703  3at  29752  llnnlt  29785  lplnnlt  29827  2llnjaN  29828  2llnjN  29829  2atnelvolN  29849  lvolnltN  29880  2lplnj  29882  dalem21  29956  dalem23  29958  dalem24  29959  dalem25  29960  dalem29  29963  dalem30  29964  dalem31N  29965  dalem32  29966  dalem33  29967  dalem34  29968  dalem35  29969  dalem36  29970  dalem37  29971  dalem40  29974  dalem46  29980  dalem47  29981  dalem58  29992  dalem59  29993  pmaple  30023  pmapglbx  30031  elpaddri  30064  paddclN  30104  pmapjoin  30114  pmapjat1  30115  pmapjat2  30116  pclun2N  30161  polcon3N  30179  2polcon4bN  30180  polcon2N  30181  paddunN  30189  poldmj1N  30190  pmapj2N  30191  pmapocjN  30192  psubclinN  30210  paddatclN  30211  poml5N  30216  osumcllem3N  30220  osumcllem4N  30221  osumcllem11N  30228  pl42lem4N  30244  lhpmcvr5N  30289  lhp2at0  30294  lhpelim  30299  lhple  30304  lautco  30359  ldilco  30378  ltrncl  30387  ltrn11  30388  ltrncnvnid  30389  ltrnle  30391  ltrncnvleN  30392  ltrnm  30393  ltrnj  30394  ltrncvr  30395  ltrnval1  30396  ltrncnvatb  30400  ltrncnvel  30404  ltrneq2  30410  trlval2  30425  trlcnv  30427  trljat1  30428  trlne  30447  cdleme8  30512  cdlemefrs29pre00  30657  cdleme42a  30733  cdlemeg49lebilem  30801  cdlemg7fvbwN  30869  ltrnco  30981  trljco  31002  trljco2  31003  tgrpov  31010  tendocl  31029  tendopl2  31039  diaord  31310  cdlemm10N  31381  dibord  31422  dicvaddcl  31453  dicvscacl  31454  dihvalcqpre  31498  dihord6apre  31519  dihord3  31520  dihord4  31521  dihmeetlem1N  31553  dihglblem3N  31558  dihmeetlem2N  31562  dihlspsnssN  31595  dihlspsnat  31596  dihglblem6  31603  dochss  31628  dochshpncl  31647  dochdmj1  31653  dochkr1  31741  dochkr1OLDN  31742  lcfl6  31763  lcfrlem16  31821  hgmapval0  32158  hgmapvvlem3  32191  hdmapglem7  32195
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