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  2966  eqeu  3069  tpssi  3929  prnebg  3943  disjprg  4172  ordelinel  4643  ordunel  4770  funopg  5448  fnco  5516  resasplit  5576  fresaunres2  5578  resdif  5659  fnimapr  5750  ftpg  5879  fsnunfv  5896  fvpr1g  5900  fvpr2g  5901  f1ocnvfvb  5980  soisores  6010  f1oiso2  6035  ovig  6158  ov6g  6174  ovg  6175  frxp  6419  poxp  6421  moriotass  6542  f1ofveu  6547  onfununi  6566  smores3  6578  smoiso  6587  smoord  6590  smogt  6592  oaord  6753  oaword  6755  omord2  6773  omcan  6775  omword  6776  omwordi  6777  oneo  6787  oeord  6794  oecan  6795  oeword  6796  oewordi  6797  nnaord  6825  nnaword  6833  nnmwordi  6841  omabslem  6852  nnneo  6857  erov  6964  ecopovtrn  6970  undifixp  7061  xpdom3  7169  mapxpen  7236  dif1enOLD  7303  dif1en  7304  fimax2g  7316  unbnn  7326  fipreima  7374  suppr  7433  unwdomg  7512  epfrs  7627  tskwe  7797  dif1card  7852  infxpenlem  7855  cdaun  8012  cdaenun  8014  ficardun  8042  infcdaabs  8046  infcda  8048  infdif2  8050  infxpdom  8051  ackbij1lem9  8068  ackbij1lem16  8075  cflim2  8103  cfslb  8106  cfsmolem  8110  coftr  8113  infpssrlem4  8146  isf34lem7  8219  hsmexlem2  8267  axcc2lem  8276  axdc3lem4  8293  axcclem  8297  winainflem  8528  tskssel  8592  tskpr  8605  tskop  8606  tskint  8620  tskxp  8622  tskmap  8623  gruop  8640  grothpw  8661  grothpwex  8662  grothomex  8664  adderpqlem  8791  mulerpqlem  8792  addassnq  8795  mulassnq  8796  mulcanenq  8797  distrnq  8798  ltsonq  8806  ltanq  8808  ltmnq  8809  genpass  8846  distrlem1pr  8862  distrlem5pr  8864  ltsopr  8869  reclem3pr  8886  ltasr  8935  axlttrn  9108  axltadd  9109  lelttr  9125  mul12  9192  add12  9239  subadd  9268  addsub  9276  npncan  9283  nppcan  9284  nppcan3  9285  pnpcan  9300  pnncan  9302  ppncan  9303  subdi  9427  ltaddsub2  9463  leaddsub2  9465  receu  9627  divass  9656  div23  9657  divcan4  9663  divsubdir  9670  divcan5  9676  divdiv32  9682  divdiv2  9686  div2sub  9799  letrp1  9812  lemul1  9822  ltmulgt12  9831  lediv1  9835  ltdiv2  9855  lediv2  9860  ltdiv23  9861  lediv23  9862  lbinfmle  9923  infmrcl  9947  rpnnen1lem5  10564  xrlelttr  10706  xrre2  10718  xrmaxlt  10729  xrmaxle  10731  qsqueeze  10747  xaddass  10788  xltadd1  10795  xmulasslem3  10825  xmulass  10826  xltmul1  10831  xadddir  10835  xrsupsslem  10845  xrinfmsslem  10846  supxrun  10854  ixxdisj  10891  ixxub  10897  ixxlb  10898  ubioc1  10925  lbico1  10926  elioo5  10928  iccsupr  10957  lbicc2  10973  ubicc2  10974  iccneg  10978  icoshft  10979  icodisj  10982  snunico  10984  prunioo  10985  iccsplit  10989  iccf1o  10999  fzen  11032  fzrevral2  11091  fzshftral  11093  fzosubel2  11137  elfznelfzo  11151  modmulnn  11224  modabs  11233  moddi  11243  modsubdir  11244  exprec  11380  expdiv  11389  expubnd  11399  sqdiv  11406  bernneq2  11465  bcval3  11556  bccmpl  11559  hashgadd  11610  hashun  11615  hashunx  11619  hashbclem  11660  ccatval1  11704  ccatval2  11705  ccatass  11709  ccatopth2  11736  ccatco  11763  s2f1o  11822  shftval2  11849  mulre  11885  elicc4abs  12082  abssubge0  12090  abssuble0  12091  caubnd  12121  climbdd  12424  sin01gt0  12750  cos01gt0  12751  sin02gt0  12752  rpnnen2lem7  12779  dvdscmul  12835  dvdscmulr  12837  dvdsle  12854  dvdsleabs  12855  dvdsexp  12864  divalglem8  12879  divalgb  12883  sadass  12942  gcdass  13004  mulgcdr  13007  gcddiv  13008  qredeq  13065  qredeu  13066  euclemma  13067  prmdvdsexpb  13074  prmexpb  13076  coprimeprodsq  13142  coprimeprodsq2  13143  pythagtriplem1  13149  pythagtriplem3  13151  pythagtriplem6  13154  pythagtriplem12  13159  pythagtriplem13  13160  pythagtriplem14  13161  pythagtriplem16  13163  pythagtriplem19  13166  pythagtrip  13167  pcmul  13184  pcdiv  13185  pcqcl  13189  pcgcd1  13209  pcgcd  13210  pcfaclem  13226  ercpbl  13733  mreintcl  13779  ismred2  13787  mrcun  13806  submrc  13812  isfunc  14020  cofulid  14046  catcisolem  14220  posasymb  14368  isposi  14372  pleval2  14381  pltval3  14383  lubprop  14396  glbprop  14401  p0le  14431  latleeqm1  14467  lubss  14507  lubun  14509  clatglbss  14513  poslubdg  14534  mrelatglb0  14570  pslem  14597  spwpr4  14622  dirtr  14640  pwspjmhm  14726  gsumccat  14746  grpinvid1  14812  grpinvid2  14813  grpinvadd  14826  grpsubadd  14835  grppncan  14838  pwsinvg  14889  divssub  14959  odeq  15147  odf1o1  15165  odf1o2  15166  slwpss  15205  sylow2blem2  15214  lsmsubg  15247  lsmcom2  15248  lsmlub  15256  lsmss1  15257  lsmss2  15259  lsmass  15261  ablfaclem3  15604  mulgass2  15669  gsumdixp  15674  dvrcan1  15755  dvrcan3  15756  isabvd  15867  abvgt0  15875  abvres  15886  islss  15970  lspss  16019  lspssp  16023  lsslsp  16050  0lmhm  16075  reslmhm2b  16089  lsmcl  16114  lsmsp2  16118  lidlnegcl  16244  lidlnz  16258  aspss  16350  evlslem4  16523  coe1sclmul  16633  coe1sclmulfv  16634  coe1sclmul2  16635  xrsdsreclblem  16703  xrsdsreclb  16704  chrcong  16769  zndvds  16789  zntoslem  16796  ocvsscon  16861  basgen  17012  clsss  17077  ntrin  17084  elcls  17096  ntrcls0  17099  neiint  17127  neiss  17132  neips  17136  opnssneib  17138  innei  17148  islp2  17168  restco  17186  restcls  17203  restntr  17204  ordtopn3  17218  ordtcld3  17221  iscnp  17259  cnconst2  17305  t1ficld  17349  cmpsublem  17420  cmpcld  17423  clscon  17450  ptpjcn  17600  ptpjopn  17601  txcn  17615  ptrescn  17628  xkopjcn  17645  kqfeq  17713  kqfvima  17719  opnfbas  17831  filin  17843  neifil  17869  filuni  17874  cfinfil  17882  ufprim  17898  filufint  17909  ufinffr  17918  fin1aufil  17921  flimclslem  17973  flfneii  17981  fcfval  18022  alexsubALT  18039  cldsubg  18097  divstgphaus  18109  tsmsxp  18141  ustref  18205  ustelimasn  18209  ustimasn  18215  trust  18216  cfiluexsm  18277  cfiluweak  18282  psmetsym  18298  psmetlecl  18303  xmetlecl  18333  xmetsym  18334  prdsxmetlem  18355  xblcntrps  18397  xblcntr  18398  blssec  18422  blpnfctr  18423  txmetcn  18535  metusttoOLD  18544  metustto  18545  nmrpcl  18623  nm2dif  18628  nminvr  18662  nmoeq0  18727  0nmhm  18746  cnmet  18763  metds0  18837  metdscn2  18844  cnmpt2pc  18910  iihalf1  18913  iihalf2  18915  icchmeo  18923  bndth  18940  pi1xfr  19037  nmhmcn  19085  cphnmvs  19110  lmmbr2  19169  cfil3i  19179  bcthlem5  19238  resscdrg  19269  ovolfioo  19321  ovolficc  19322  ovolsscl  19339  ovolssnul  19340  ovoliunlem2  19356  volun  19396  iundisj2  19400  iunmbl2  19408  ovolioo  19419  itg2const  19589  cniccibl  19689  limcfval  19716  dvid  19761  dvnp1  19768  dvfsum2  19875  evlsval  19897  tdeglem3  19939  mdegmullem  19958  deg1scl  19993  deg1mul3le  19996  ig1pval3  20054  ig1pdvds  20056  ply1term  20080  coe1term  20134  dgradd2  20143  dvply1  20158  facth  20180  quotcan  20183  dvtaylp  20243  ptolemy  20361  sinq12gt0  20372  sincosq1eq  20377  efgh  20400  explog  20445  argrege0  20463  logimul  20466  logmul2  20468  logdiv2  20469  angcan  20601  ang180lem2  20609  ang180lem3  20610  pythag  20616  logrec  20618  isosctrlem1  20619  isosctrlem2  20620  angpieqvd  20629  mumullem2  20920  lgsval4  21057  lgsmod  21062  padicabv  21281  nbusgrafi  21415  nb3graprlem2  21418  nb3grapr  21419  nb3grapr2  21420  cusgra3v  21430  cusgrasizeindslem3  21441  spthonepeq  21544  1pthon  21548  constr2spth  21557  constr2pth  21558  2pthon  21559  3v3e3cycl1  21588  constr3lem5  21592  constr3trllem2  21595  constr3trllem3  21596  constr3trllem5  21598  vdgrf  21626  vdusgra0nedg  21636  hashnbgravd  21638  iseupa  21644  grpoinvid1  21775  grpoinvid2  21776  grpoasscan1  21782  grpoasscan2  21783  grpoinvop  21786  grpopncan  21796  grponpcan  21797  grpopnpcan2  21798  gxcl  21810  gxinv  21815  gxinv2  21816  gxsuc  21817  gxid  21818  gxnn0add  21819  gxnn0mul  21822  ablonncan  21839  issubgoi  21855  ablomul  21900  zerdivemp1  21979  rngoridfz  21980  vcsubdir  21992  vcnegsubdi2  22011  vcoprnelem  22014  isvc  22017  isnv  22048  nvscom  22067  nvmul0or  22090  nvpncan2  22094  nvaddsub4  22099  nvnncan  22101  nvdif  22111  nvpi  22112  nvabs  22119  nv1  22122  imsmetlem  22139  0oval  22246  lnon0  22256  blometi  22261  ajfval  22267  ipasslem5  22293  ajval  22320  hlipgt0  22373  ssphl  22376  hvadd12  22494  hvmulcom  22502  hvsubass  22503  hvsubdistr1  22508  hvsubdistr2  22509  hvaddcan2  22530  hvmulcan  22531  hvmulcan2  22532  hvsubcan  22533  hvsubcan2  22534  his7  22549  his2sub  22551  his2sub2  22552  bcs2  22641  bcs3  22642  hhssnv  22721  chj12  22993  spansncol  23027  cm2j  23079  homul12  23265  hoaddsub  23276  unopf1o  23376  adj2  23394  braadd  23405  kbmul  23415  eigvalcl  23421  lnopmulsubi  23436  hmopco  23483  cnlnadjlem2  23528  adjlnop  23546  leopmul  23594  leoptr  23597  hstoh  23692  strlem3a  23712  hstrlem3a  23720  cvntr  23752  dmdsl3  23775  atexch  23841  atcvatlem  23845  mdsymlem5  23867  cdj3lem2  23895  cdj3lem3  23898  iundisj2f  23987  curry2ima  24054  iocinioc2  24099  iundisj2fi  24110  divnumden2  24118  xreceu  24125  logeq0im1  24351  logccne0OLD  24352  logccne0  24353  logbid1  24355  logblt  24363  indfval  24371  measle0  24519  measres  24533  volfiniune  24543  sitgclbn  24614  cndprobtot  24651  cndprobnul  24652  cndprobprob  24653  ballotlemsgt1  24725  ballotlemrv1  24735  ballotlemrv2  24736  ballotlemfrcn0  24744  ghomgsg  25061  ghomf1olem  25062  lediv2aALT  25074  mulcan1g  25146  mulsuble0b  25150  prodfn0  25179  prodfrec  25180  ntrivcvgfvn0  25184  fprodabs  25254  fprodefsum  25255  iprodefisumlem  25274  binomrisefac  25313  dvdspw  25321  fununiq  25344  trpredpo  25456  wfrlem3  25476  wfrlem4  25477  wfrlem9  25482  sltres  25536  nodenselem8  25560  nocvxmin  25563  nofulllem3  25576  nofulllem4  25577  brbtwn2  25752  axcgrid  25763  axsegconlem6  25769  axsegconlem7  25770  axsegconlem8  25771  axsegconlem9  25772  axsegconlem10  25773  ax5seglem1  25775  ax5seglem2  25776  axpasch  25788  axlowdimlem14  25802  axlowdimlem16  25804  axeuclidlem  25809  axcontlem2  25812  axcontlem5  25815  lineext  25918  linecgr  25923  lineelsb2  25990  bpolycl  26006  cnicciblnc  26179  areacirclem4  26187  areacirclem5  26189  areacirclem6  26190  clsun  26225  neiin  26229  ivthALT  26232  fness  26256  neifg  26294  eltail  26297  fzmul  26338  heiborlem3  26416  exidreslem  26446  ghomco  26452  rngoneglmul  26461  zerdivemp1x  26465  isdrngo2  26468  rngogrphom  26481  smprngopr  26556  eldioph2  26714  elmapresaun  26723  dvdsrabdioph  26764  rabrenfdioph  26769  pellexlem5  26790  pellex  26792  pell14qrdivcl  26822  pell14qrgapw  26833  pellfund14gap  26844  reglogmul  26850  reglogexp  26851  monotoddzzfi  26899  monotoddzz  26900  zindbi  26903  jm2.17a  26919  jm2.17b  26920  congadd  26925  dvdsleabs2  26949  dvdsabsmod0  26951  jm2.19lem2  26955  jm2.19lem3  26956  jm2.19  26958  jm2.22  26960  jm2.23  26961  jm2.16nn0  26969  rmydioph  26979  rmxdiophlem  26980  jm3.1  26985  islssfgi  27042  pwssplit0  27059  pwssplit4  27063  uvcval  27106  uvcresum  27114  frlmsslsp  27120  f1lindf  27164  lnrfgtr  27196  hbtlem5  27204  pmtrval  27266  pmtrrn  27271  dvconstbi  27423  refsumcn  27572  fmuldfeq  27584  climsuselem1  27604  ibliccsinexp  27616  stoweidlem10  27630  stoweidlem14  27634  stoweidlem20  27640  stoweidlem22  27642  stoweidlem28  27648  stoweidlem31  27651  stoweidlem34  27654  stoweidlem56  27676  stoweidlem59  27679  sigaraf  27714  sigarmf  27715  sigarls  27718  el2xptp0  27953  otthg  27956  2f1fvneq  27962  f13dfv  27966  leaddsuble  27974  elfzmlbm  27981  2elfz3nn0  27988  fzo1fzo0n0  27992  swrdswrd  28015  swrdccatin12lem2  28024  swrdccatin12lem3a  28025  swrdccatin12lem3b  28026  swrdccatin12lem3  28028  swrdccatin12  28030  nbfiusgrafi  28038  usgra2wlkspthlem1  28040  usgra2wlkspth  28042  2wlkonot3v  28076  2spthonot3v  28077  usg2wlkonot  28084  usg2wotspth  28085  2pthwlkonot  28086  2spontn0vne  28088  usg2spthonot0  28090  frgra3v  28110  3vfriswmgra  28113  vdfrgra0  28130  vdgfrgra0  28131  vdn0frgrav2  28132  vdn1frgrav2  28134  frg2woteu  28162  frg2wot1  28164  frg2woteq  28167  usg2spot2nb  28172  usgreghash2spot  28176  reccot  28219  rectan  28220  chordthmALT  28759  bnj553  28979  bnj966  29025  bnj967  29026  bnj1125  29071  bnj1173  29081  lubunNEW  29460  lsmsat  29495  lsmsatcv  29497  lcvexchlem4  29524  lcvexchlem5  29525  lfli  29548  lflcl  29551  lflmul  29555  lfl1  29557  eqlkr  29586  lshpkrlem4  29600  opcon3b  29683  oplecon3b  29687  oplecon1b  29688  opltcon3b  29691  opltcon1b  29692  oldmm1  29704  oldmm2  29705  oldmj1  29708  oldmj2  29709  olj01  29712  omllaw2N  29731  omllaw3  29732  cmtcomlemN  29735  omlfh1N  29745  omlfh3N  29746  cvrnbtwn2  29762  cvrnbtwn3  29763  cvrcon3b  29764  cvrnbtwn4  29766  leatb  29779  atcmp  29798  atnlt  29800  atcvreq0  29801  atncvrN  29802  atnle  29804  atlatle  29807  cvlexchb1  29817  hlrelat5N  29887  atcvr0eq  29912  lnnat  29913  atexchltN  29927  3at  29976  llnnlt  30009  lplnnlt  30051  2llnjaN  30052  2llnjN  30053  2atnelvolN  30073  lvolnltN  30104  2lplnj  30106  dalem21  30180  dalem23  30182  dalem24  30183  dalem25  30184  dalem29  30187  dalem30  30188  dalem31N  30189  dalem32  30190  dalem33  30191  dalem34  30192  dalem35  30193  dalem36  30194  dalem37  30195  dalem40  30198  dalem46  30204  dalem47  30205  dalem58  30216  dalem59  30217  pmaple  30247  pmapglbx  30255  elpaddri  30288  paddclN  30328  pmapjoin  30338  pmapjat1  30339  pmapjat2  30340  pclun2N  30385  polcon3N  30403  2polcon4bN  30404  polcon2N  30405  paddunN  30413  poldmj1N  30414  pmapj2N  30415  pmapocjN  30416  psubclinN  30434  paddatclN  30435  poml5N  30440  osumcllem3N  30444  osumcllem4N  30445  osumcllem11N  30452  pl42lem4N  30468  lhpmcvr5N  30513  lhp2at0  30518  lhpelim  30523  lhple  30528  lautco  30583  ldilco  30602  ltrncl  30611  ltrn11  30612  ltrncnvnid  30613  ltrnle  30615  ltrncnvleN  30616  ltrnm  30617  ltrnj  30618  ltrncvr  30619  ltrnval1  30620  ltrncnvatb  30624  ltrncnvel  30628  ltrneq2  30634  trlval2  30649  trlcnv  30651  trljat1  30652  trlne  30671  cdleme8  30736  cdlemefrs29pre00  30881  cdleme42a  30957  cdlemeg49lebilem  31025  cdlemg7fvbwN  31093  ltrnco  31205  trljco  31226  trljco2  31227  tgrpov  31234  tendocl  31253  tendopl2  31263  diaord  31534  cdlemm10N  31605  dibord  31646  dicvaddcl  31677  dicvscacl  31678  dihvalcqpre  31722  dihord6apre  31743  dihord3  31744  dihord4  31745  dihmeetlem1N  31777  dihglblem3N  31782  dihmeetlem2N  31786  dihlspsnssN  31819  dihlspsnat  31820  dihglblem6  31827  dochss  31852  dochshpncl  31871  dochdmj1  31877  dochkr1  31965  dochkr1OLDN  31966  lcfl6  31987  lcfrlem16  32045  hgmapval0  32382  hgmapvvlem3  32415  hdmapglem7  32419
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