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

Theorem 3adant3 977
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 954 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 16 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  vtoclgft  2962  eqeu  3065  tpssi  3925  prnebg  3939  disjprg  4168  ordelinel  4639  ordunel  4766  funopg  5444  fnco  5512  resasplit  5572  fresaunres2  5574  resdif  5655  fnimapr  5746  ftpg  5875  fsnunfv  5892  fvpr1g  5896  fvpr2g  5897  f1ocnvfvb  5976  soisores  6006  f1oiso2  6031  ovig  6154  ov6g  6170  ovg  6171  frxp  6415  poxp  6417  moriotass  6538  f1ofveu  6543  onfununi  6562  smores3  6574  smoiso  6583  smoord  6586  smogt  6588  oaord  6749  oaword  6751  omord2  6769  omcan  6771  omword  6772  omwordi  6773  oneo  6783  oeord  6790  oecan  6791  oeword  6792  oewordi  6793  nnaord  6821  nnaword  6829  nnmwordi  6837  omabslem  6848  nnneo  6853  erov  6960  ecopovtrn  6966  undifixp  7057  xpdom3  7165  mapxpen  7232  dif1enOLD  7299  dif1en  7300  fimax2g  7312  unbnn  7322  fipreima  7370  suppr  7429  unwdomg  7508  epfrs  7623  tskwe  7793  dif1card  7848  infxpenlem  7851  cdaun  8008  cdaenun  8010  ficardun  8038  infcdaabs  8042  infcda  8044  infdif2  8046  infxpdom  8047  ackbij1lem9  8064  ackbij1lem16  8071  cflim2  8099  cfslb  8102  cfsmolem  8106  coftr  8109  infpssrlem4  8142  isf34lem7  8215  hsmexlem2  8263  axcc2lem  8272  axdc3lem4  8289  axcclem  8293  winainflem  8524  tskssel  8588  tskpr  8601  tskop  8602  tskint  8616  tskxp  8618  tskmap  8619  gruop  8636  grothpw  8657  grothpwex  8658  grothomex  8660  adderpqlem  8787  mulerpqlem  8788  addassnq  8791  mulassnq  8792  mulcanenq  8793  distrnq  8794  ltsonq  8802  ltanq  8804  ltmnq  8805  genpass  8842  distrlem1pr  8858  distrlem5pr  8860  ltsopr  8865  reclem3pr  8882  ltasr  8931  axlttrn  9104  axltadd  9105  lelttr  9121  mul12  9188  add12  9235  subadd  9264  addsub  9272  npncan  9279  nppcan  9280  nppcan3  9281  pnpcan  9296  pnncan  9298  ppncan  9299  subdi  9423  ltaddsub2  9459  leaddsub2  9461  receu  9623  divass  9652  div23  9653  divcan4  9659  divsubdir  9666  divcan5  9672  divdiv32  9678  divdiv2  9682  div2sub  9795  letrp1  9808  lemul1  9818  ltmulgt12  9827  lediv1  9831  ltdiv2  9851  lediv2  9856  ltdiv23  9857  lediv23  9858  lbinfmle  9919  infmrcl  9943  rpnnen1lem5  10560  xrlelttr  10702  xrre2  10714  xrmaxlt  10725  xrmaxle  10727  qsqueeze  10743  xaddass  10784  xltadd1  10791  xmulasslem3  10821  xmulass  10822  xltmul1  10827  xadddir  10831  xrsupsslem  10841  xrinfmsslem  10842  supxrun  10850  ixxdisj  10887  ixxub  10893  ixxlb  10894  ubioc1  10921  lbico1  10922  elioo5  10924  iccsupr  10953  lbicc2  10969  ubicc2  10970  iccneg  10974  icoshft  10975  icodisj  10978  snunico  10980  prunioo  10981  iccsplit  10985  iccf1o  10995  fzen  11028  fzrevral2  11087  fzshftral  11089  fzosubel2  11133  elfznelfzo  11147  modmulnn  11220  modabs  11229  moddi  11239  modsubdir  11240  exprec  11376  expdiv  11385  expubnd  11395  sqdiv  11402  bernneq2  11461  bcval3  11552  bccmpl  11555  hashgadd  11606  hashun  11611  hashunx  11615  hashbclem  11656  ccatval1  11700  ccatval2  11701  ccatass  11705  ccatopth2  11732  ccatco  11759  s2f1o  11818  shftval2  11845  mulre  11881  elicc4abs  12078  abssubge0  12086  abssuble0  12087  caubnd  12117  climbdd  12420  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  rpnnen2lem7  12775  dvdscmul  12831  dvdscmulr  12833  dvdsle  12850  dvdsleabs  12851  dvdsexp  12860  divalglem8  12875  divalgb  12879  sadass  12938  gcdass  13000  mulgcdr  13003  gcddiv  13004  qredeq  13061  qredeu  13062  euclemma  13063  prmdvdsexpb  13070  prmexpb  13072  coprimeprodsq  13138  coprimeprodsq2  13139  pythagtriplem1  13145  pythagtriplem3  13147  pythagtriplem6  13150  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  pythagtriplem19  13162  pythagtrip  13163  pcmul  13180  pcdiv  13181  pcqcl  13185  pcgcd1  13205  pcgcd  13206  pcfaclem  13222  ercpbl  13729  mreintcl  13775  ismred2  13783  mrcun  13802  submrc  13808  isfunc  14016  cofulid  14042  catcisolem  14216  posasymb  14364  isposi  14368  pleval2  14377  pltval3  14379  lubprop  14392  glbprop  14397  p0le  14427  latleeqm1  14463  lubss  14503  lubun  14505  clatglbss  14509  poslubdg  14530  mrelatglb0  14566  pslem  14593  spwpr4  14618  dirtr  14636  pwspjmhm  14722  gsumccat  14742  grpinvid1  14808  grpinvid2  14809  grpinvadd  14822  grpsubadd  14831  grppncan  14834  pwsinvg  14885  divssub  14955  odeq  15143  odf1o1  15161  odf1o2  15162  slwpss  15201  sylow2blem2  15210  lsmsubg  15243  lsmcom2  15244  lsmlub  15252  lsmss1  15253  lsmss2  15255  lsmass  15257  ablfaclem3  15600  mulgass2  15665  gsumdixp  15670  dvrcan1  15751  dvrcan3  15752  isabvd  15863  abvgt0  15871  abvres  15882  islss  15966  lspss  16015  lspssp  16019  lsslsp  16046  0lmhm  16071  reslmhm2b  16085  lsmcl  16110  lsmsp2  16114  lidlnegcl  16240  lidlnz  16254  aspss  16346  evlslem4  16519  coe1sclmul  16629  coe1sclmulfv  16630  coe1sclmul2  16631  xrsdsreclblem  16699  xrsdsreclb  16700  chrcong  16765  zndvds  16785  zntoslem  16792  ocvsscon  16857  basgen  17008  clsss  17073  ntrin  17080  elcls  17092  ntrcls0  17095  neiint  17123  neiss  17128  neips  17132  opnssneib  17134  innei  17144  islp2  17164  restco  17182  restcls  17199  restntr  17200  ordtopn3  17214  ordtcld3  17217  iscnp  17255  cnconst2  17301  t1ficld  17345  cmpsublem  17416  cmpcld  17419  clscon  17446  ptpjcn  17596  ptpjopn  17597  txcn  17611  ptrescn  17624  xkopjcn  17641  kqfeq  17709  kqfvima  17715  opnfbas  17827  filin  17839  neifil  17865  filuni  17870  cfinfil  17878  ufprim  17894  filufint  17905  ufinffr  17914  fin1aufil  17917  flimclslem  17969  flfneii  17977  fcfval  18018  alexsubALT  18035  cldsubg  18093  divstgphaus  18105  tsmsxp  18137  ustref  18201  ustelimasn  18205  ustimasn  18211  trust  18212  cfiluexsm  18273  cfiluweak  18278  psmetsym  18294  psmetlecl  18299  xmetlecl  18329  xmetsym  18330  prdsxmetlem  18351  xblcntrps  18393  xblcntr  18394  blssec  18418  blpnfctr  18419  txmetcn  18531  metusttoOLD  18540  metustto  18541  nmrpcl  18619  nm2dif  18624  nminvr  18658  nmoeq0  18723  0nmhm  18742  cnmet  18759  metds0  18833  metdscn2  18840  cnmpt2pc  18906  iihalf1  18909  iihalf2  18911  icchmeo  18919  bndth  18936  pi1xfr  19033  nmhmcn  19081  cphnmvs  19106  lmmbr2  19165  cfil3i  19175  bcthlem5  19234  resscdrg  19265  ovolfioo  19317  ovolficc  19318  ovolsscl  19335  ovolssnul  19336  ovoliunlem2  19352  volun  19392  iundisj2  19396  iunmbl2  19404  ovolioo  19415  itg2const  19585  cniccibl  19685  limcfval  19712  dvid  19757  dvnp1  19764  dvfsum2  19871  evlsval  19893  tdeglem3  19935  mdegmullem  19954  deg1scl  19989  deg1mul3le  19992  ig1pval3  20050  ig1pdvds  20052  ply1term  20076  coe1term  20130  dgradd2  20139  dvply1  20154  facth  20176  quotcan  20179  dvtaylp  20239  ptolemy  20357  sinq12gt0  20368  sincosq1eq  20373  efgh  20396  explog  20441  argrege0  20459  logimul  20462  logmul2  20464  logdiv2  20465  angcan  20597  ang180lem2  20605  ang180lem3  20606  pythag  20612  logrec  20614  isosctrlem1  20615  isosctrlem2  20616  angpieqvd  20625  mumullem2  20916  lgsval4  21053  lgsmod  21058  padicabv  21277  nbusgrafi  21411  nb3graprlem2  21414  nb3grapr  21415  nb3grapr2  21416  cusgra3v  21426  cusgrasizeindslem3  21437  spthonepeq  21540  1pthon  21544  constr2spth  21553  constr2pth  21554  2pthon  21555  3v3e3cycl1  21584  constr3lem5  21588  constr3trllem2  21591  constr3trllem3  21592  constr3trllem5  21594  vdgrf  21622  vdusgra0nedg  21632  hashnbgravd  21634  iseupa  21640  grpoinvid1  21771  grpoinvid2  21772  grpoasscan1  21778  grpoasscan2  21779  grpoinvop  21782  grpopncan  21792  grponpcan  21793  grpopnpcan2  21794  gxcl  21806  gxinv  21811  gxinv2  21812  gxsuc  21813  gxid  21814  gxnn0add  21815  gxnn0mul  21818  ablonncan  21835  issubgoi  21851  ablomul  21896  zerdivemp1  21975  rngoridfz  21976  vcsubdir  21988  vcnegsubdi2  22007  vcoprnelem  22010  isvc  22013  isnv  22044  nvscom  22063  nvmul0or  22086  nvpncan2  22090  nvaddsub4  22095  nvnncan  22097  nvdif  22107  nvpi  22108  nvabs  22115  nv1  22118  imsmetlem  22135  0oval  22242  lnon0  22252  blometi  22257  ajfval  22263  ipasslem5  22289  ajval  22316  hlipgt0  22369  ssphl  22372  hvadd12  22490  hvmulcom  22498  hvsubass  22499  hvsubdistr1  22504  hvsubdistr2  22505  hvaddcan2  22526  hvmulcan  22527  hvmulcan2  22528  hvsubcan  22529  hvsubcan2  22530  his7  22545  his2sub  22547  his2sub2  22548  bcs2  22637  bcs3  22638  hhssnv  22717  chj12  22989  spansncol  23023  cm2j  23075  homul12  23261  hoaddsub  23272  unopf1o  23372  adj2  23390  braadd  23401  kbmul  23411  eigvalcl  23417  lnopmulsubi  23432  hmopco  23479  cnlnadjlem2  23524  adjlnop  23542  leopmul  23590  leoptr  23593  hstoh  23688  strlem3a  23708  hstrlem3a  23716  cvntr  23748  dmdsl3  23771  atexch  23837  atcvatlem  23841  mdsymlem5  23863  cdj3lem2  23891  cdj3lem3  23894  iundisj2f  23983  curry2ima  24050  iocinioc2  24095  iundisj2fi  24106  divnumden2  24114  xreceu  24121  logeq0im1  24347  logccne0OLD  24348  logccne0  24349  logbid1  24351  logblt  24359  indfval  24367  measle0  24515  measres  24529  volfiniune  24539  sitgclbn  24610  cndprobtot  24647  cndprobnul  24648  cndprobprob  24649  ballotlemsgt1  24721  ballotlemrv1  24731  ballotlemrv2  24732  ballotlemfrcn0  24740  ghomgsg  25057  ghomf1olem  25058  lediv2aALT  25070  mulcan1g  25142  mulsuble0b  25146  prodfn0  25175  prodfrec  25176  ntrivcvgfvn0  25180  fprodabs  25250  fprodefsum  25251  iprodefisumlem  25270  binomrisefac  25309  dvdspw  25317  fununiq  25340  trpredpo  25452  wfrlem3  25472  wfrlem4  25473  wfrlem9  25478  sltres  25532  nodenselem8  25556  nocvxmin  25559  nofulllem3  25572  nofulllem4  25573  brbtwn2  25748  axcgrid  25759  axsegconlem6  25765  axsegconlem7  25766  axsegconlem8  25767  axsegconlem9  25768  axsegconlem10  25769  ax5seglem1  25771  ax5seglem2  25772  axpasch  25784  axlowdimlem14  25798  axlowdimlem16  25800  axeuclidlem  25805  axcontlem2  25808  axcontlem5  25811  lineext  25914  linecgr  25919  lineelsb2  25986  bpolycl  26002  cnicciblnc  26175  areacirclem4  26183  areacirclem5  26185  areacirclem6  26186  clsun  26221  neiin  26225  ivthALT  26228  fness  26252  neifg  26290  eltail  26293  fzmul  26334  heiborlem3  26412  exidreslem  26442  ghomco  26448  rngoneglmul  26457  zerdivemp1x  26461  isdrngo2  26464  rngogrphom  26477  smprngopr  26552  eldioph2  26710  elmapresaun  26719  dvdsrabdioph  26760  rabrenfdioph  26765  pellexlem5  26786  pellex  26788  pell14qrdivcl  26818  pell14qrgapw  26829  pellfund14gap  26840  reglogmul  26846  reglogexp  26847  monotoddzzfi  26895  monotoddzz  26896  zindbi  26899  jm2.17a  26915  jm2.17b  26916  congadd  26921  dvdsleabs2  26945  dvdsabsmod0  26947  jm2.19lem2  26951  jm2.19lem3  26952  jm2.19  26954  jm2.22  26956  jm2.23  26957  jm2.16nn0  26965  rmydioph  26975  rmxdiophlem  26976  jm3.1  26981  islssfgi  27038  pwssplit0  27055  pwssplit4  27059  uvcval  27102  uvcresum  27110  frlmsslsp  27116  f1lindf  27160  lnrfgtr  27192  hbtlem5  27200  pmtrval  27262  pmtrrn  27267  dvconstbi  27419  refsumcn  27568  fmuldfeq  27580  climsuselem1  27600  ibliccsinexp  27612  stoweidlem10  27626  stoweidlem14  27630  stoweidlem20  27636  stoweidlem22  27638  stoweidlem28  27644  stoweidlem31  27647  stoweidlem34  27650  stoweidlem56  27672  stoweidlem59  27675  sigaraf  27710  sigarmf  27711  sigarls  27714  el2xptp0  27949  otthg  27952  2f1fvneq  27958  f13dfv  27962  leaddsuble  27970  elfzmlbm  27977  2elfz3nn0  27984  fzo1fzo0n0  27988  swrdswrd  28011  swrdccatin12lem2  28020  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccatin12  28026  nbfiusgrafi  28034  usgra2wlkspthlem1  28036  usgra2wlkspth  28038  2wlkonot3v  28072  2spthonot3v  28073  usg2wlkonot  28080  usg2wotspth  28081  2pthwlkonot  28082  2spontn0vne  28084  usg2spthonot0  28086  frgra3v  28106  3vfriswmgra  28109  vdfrgra0  28126  vdgfrgra0  28127  vdn0frgrav2  28128  vdn1frgrav2  28130  frg2woteu  28158  frg2wot1  28160  frg2woteq  28163  usg2spot2nb  28168  usgreghash2spot  28172  reccot  28215  rectan  28216  chordthmALT  28755  bnj553  28975  bnj966  29021  bnj967  29022  bnj1125  29067  bnj1173  29077  lubunNEW  29456  lsmsat  29491  lsmsatcv  29493  lcvexchlem4  29520  lcvexchlem5  29521  lfli  29544  lflcl  29547  lflmul  29551  lfl1  29553  eqlkr  29582  lshpkrlem4  29596  opcon3b  29679  oplecon3b  29683  oplecon1b  29684  opltcon3b  29687  opltcon1b  29688  oldmm1  29700  oldmm2  29701  oldmj1  29704  oldmj2  29705  olj01  29708  omllaw2N  29727  omllaw3  29728  cmtcomlemN  29731  omlfh1N  29741  omlfh3N  29742  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrcon3b  29760  cvrnbtwn4  29762  leatb  29775  atcmp  29794  atnlt  29796  atcvreq0  29797  atncvrN  29798  atnle  29800  atlatle  29803  cvlexchb1  29813  hlrelat5N  29883  atcvr0eq  29908  lnnat  29909  atexchltN  29923  3at  29972  llnnlt  30005  lplnnlt  30047  2llnjaN  30048  2llnjN  30049  2atnelvolN  30069  lvolnltN  30100  2lplnj  30102  dalem21  30176  dalem23  30178  dalem24  30179  dalem25  30180  dalem29  30183  dalem30  30184  dalem31N  30185  dalem32  30186  dalem33  30187  dalem34  30188  dalem35  30189  dalem36  30190  dalem37  30191  dalem40  30194  dalem46  30200  dalem47  30201  dalem58  30212  dalem59  30213  pmaple  30243  pmapglbx  30251  elpaddri  30284  paddclN  30324  pmapjoin  30334  pmapjat1  30335  pmapjat2  30336  pclun2N  30381  polcon3N  30399  2polcon4bN  30400  polcon2N  30401  paddunN  30409  poldmj1N  30410  pmapj2N  30411  pmapocjN  30412  psubclinN  30430  paddatclN  30431  poml5N  30436  osumcllem3N  30440  osumcllem4N  30441  osumcllem11N  30448  pl42lem4N  30464  lhpmcvr5N  30509  lhp2at0  30514  lhpelim  30519  lhple  30524  lautco  30579  ldilco  30598  ltrncl  30607  ltrn11  30608  ltrncnvnid  30609  ltrnle  30611  ltrncnvleN  30612  ltrnm  30613  ltrnj  30614  ltrncvr  30615  ltrnval1  30616  ltrncnvatb  30620  ltrncnvel  30624  ltrneq2  30630  trlval2  30645  trlcnv  30647  trljat1  30648  trlne  30667  cdleme8  30732  cdlemefrs29pre00  30877  cdleme42a  30953  cdlemeg49lebilem  31021  cdlemg7fvbwN  31089  ltrnco  31201  trljco  31222  trljco2  31223  tgrpov  31230  tendocl  31249  tendopl2  31259  diaord  31530  cdlemm10N  31601  dibord  31642  dicvaddcl  31673  dicvscacl  31674  dihvalcqpre  31718  dihord6apre  31739  dihord3  31740  dihord4  31741  dihmeetlem1N  31773  dihglblem3N  31778  dihmeetlem2N  31782  dihlspsnssN  31815  dihlspsnat  31816  dihglblem6  31823  dochss  31848  dochshpncl  31867  dochdmj1  31873  dochkr1  31961  dochkr1OLDN  31962  lcfl6  31983  lcfrlem16  32041  hgmapval0  32378  hgmapvvlem3  32411  hdmapglem7  32415
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator