MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant1 Structured version   Visualization version   GIF version

Theorem 3adant1 1122
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
Hypothesis
Ref Expression
3adant.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
3adant1 ((𝜃𝜑𝜓) → 𝜒)

Proof of Theorem 3adant1
StepHypRef Expression
1 3adant.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantll 710 . 2 (((𝜃𝜑) ∧ 𝜓) → 𝜒)
323impa 1102 1 ((𝜃𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1081
This theorem is referenced by:  3ad2ant2  1126  3ad2ant3  1127  3simpc  1142  eupickb  2716  spc3egv  3603  sbciegft  3807  reuhyp  5312  funopg  6383  funprg  6402  funtpg  6403  funcnvtp  6411  unima  6733  fvun1  6748  fnreseql  6811  xpprsng  6895  ftpg  6911  f13dfv  7022  mpoeq3ia  7221  ordunel  7530  fex2  7626  funexw  7644  poxp  7813  suppval1  7827  wfr3g  7944  smores3  7981  oaord  8163  oacan  8164  oaword  8165  omord  8184  omcan  8185  omwordri  8188  odi  8195  omass  8196  oeord  8204  oecan  8205  oewordri  8208  oeordsuc  8210  nnaord  8235  nnaordr  8236  nndi  8239  nnmass  8240  nnaword  8243  nnmord  8248  nnmwordri  8252  erov  8384  ecopovtrn  8390  ixpf  8473  mapxpen  8672  fimax2g  8753  unbnn  8763  funisfsupp  8827  inelfi  8871  elfiun  8883  sup0  8919  suppr  8924  infpr  8956  r111  9193  dif1card  9425  ackbij1lem16  9646  cff1  9669  cfflb  9670  cfsmolem  9681  fin23lem34  9757  hsmexlem2  9838  axcc3  9849  domtriomlem  9853  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  konigthlem  9979  gchdomtri  10040  tskpr  10181  tskop  10182  tskuni  10194  tskun  10197  gruop  10216  gruun  10217  grudomon  10228  adderpqlem  10365  mulerpqlem  10366  addassnq  10369  mulassnq  10370  distrnq  10372  ltsonq  10380  ltanq  10382  ltmnq  10383  genpass  10420  distrlem1pr  10436  distrlem4pr  10437  ltsopr  10443  adddir  10621  axlttrn  10702  ltletr  10721  letr  10723  mul32  10795  mul31  10796  add32  10847  subsub23  10880  addsubass  10885  subcan2  10900  subsub2  10903  nppcan2  10906  sub32  10909  nnncan  10910  nnncan2  10912  pnpcan2  10915  subdi  11062  subdir  11063  receu  11274  mulcan1g  11282  mulcan2g  11283  divmul3  11292  divrec  11303  divrec2  11304  divsubdir  11323  subdivcomb2  11325  divdiv1  11340  redivcl  11348  div2neg  11352  ltmul2  11480  lemul1  11481  lemul2  11482  lemul2a  11484  lediv1  11494  gt0div  11495  ge0div  11496  mulsuble0b  11501  ltdivmul  11504  ledivmul  11505  ltdivmul2  11506  ledivmul2  11508  lemuldiv  11509  ltdiv23  11520  lediv23  11521  ledivp1i  11554  ltdivp1i  11555  uzind2  12064  nn0ind  12066  fnn0ind  12070  uz3m2nn  12280  xrltletr  12540  xrletr  12541  xrre2  12553  xrltmin  12565  xrlemin  12567  xleadd2a  12637  xleadd1  12638  xltadd2  12640  xmulasslem3  12669  xmulass  12670  xltmul2  12676  ixxdisj  12743  iooneg  12847  iccneg  12848  icoshft  12849  icoshftf1o  12850  icodisj  12852  snunioo  12854  fzen  12914  ssfzunsnext  12942  fzrev3  12963  2ffzeq  13018  fzoaddel2  13083  elfzodifsumelfzo  13093  ssfzoulel  13121  ssfzo12bi  13122  fzoshftral  13144  adddivflid  13178  flltdivnn0lt  13193  ltdifltdiv  13194  fldiv4p1lem1div2  13195  modcyc  13264  modcyc2  13265  modaddabs  13267  modsubmodmod  13288  modaddmodup  13292  modaddmulmod  13296  moddi  13297  modsubdir  13298  expdiv  13470  digit2  13587  nfile  13710  hashdifpr  13766  hashgt23el  13775  hashreshashfun  13790  fi1uzind  13845  ccatval1  13920  ccatass  13932  swrdval  13995  swrdnd  14006  swrd0  14010  swrdfv2  14013  pfxsuff1eqwrdeq  14051  swrdswrdlem  14056  pfxccatin12lem2a  14079  pfxccatin12lem1  14080  repswccat  14138  cshwidxmod  14155  cshwidxmodr  14156  cshf1  14162  repswcshw  14164  2cshw  14165  2cshwcom  14168  2cshwcshw  14177  cshwcsh2id  14180  ccatco  14187  2swrd2eqwrdeq  14305  wwlktovf  14310  brcnvtrclfv  14353  shftval2  14424  mulre  14470  absdiv  14645  absdiflt  14667  absdifle  14668  abs3dif  14681  cau3  14705  ello12r  14864  elo12r  14875  modfsummods  15138  geoisum1c  15226  rpnnen2lem4  15560  rpnnen2lem7  15563  dvdsmulc  15627  dvdsmulcr  15629  dvdsmultr1  15637  dvdsmultr2  15639  dvdssub2  15641  oexpneg  15684  divalgb  15745  ndvdsadd  15751  sadass  15810  modgcd  15870  dvdsgcd  15882  dvdsgcdb  15883  gcdass  15885  mulgcd  15886  absmulgcd  15887  rpmulgcd  15896  nn0seqcvgd  15904  algcvga  15913  lcmdvdsb  15947  lcmass  15948  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  coprmdvds  15987  coprmdvds2  15988  rpmul  15993  cncongr1  16001  cncongr2  16002  qnumdenbi  16074  modprm0  16132  coprimeprodsq  16135  pythagtriplem4  16146  pythagtriplem8  16150  pythagtriplem9  16151  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  pcpremul  16170  pcgcd  16204  vdwapval  16299  vdwapun  16300  prmgaplem3  16379  prmgaplem4  16380  prmgaplem7  16383  prmgapprmolem  16387  mreiincl  16857  mreincl  16860  mremre  16865  mrcss  16877  catcisolem  17356  pleval2  17565  pospo  17573  latlem  17649  latjcom  17659  latmcom  17675  lubss  17721  lubun  17723  clatglbss  17727  ipole  17758  ipolt  17759  pslem  17806  dirtr  17836  gsumsgrpccat  17994  gsumws2  17997  frmdmnd  18014  isgrpi  18066  grpsubrcan  18120  grpinvsub  18121  grpsubeq0  18125  grpsubadd0sub  18126  grpnpcan  18131  qussub  18280  ghmsub  18306  symggrplem  18458  symggrp  18460  symgextsymg  18483  gsmsymgreqlem2  18490  symgfixfolem1  18497  pmtrprfv3  18513  symggen  18529  lsmass  18726  efgsrel  18791  cntzcmn  18891  dvrcl  19367  unitdvcl  19368  dvrcan1  19372  subrgmre  19490  abvsubtri  19537  abvtrivd  19542  lmodvsubval2  19620  rmodislmodlem  19632  rmodislmod  19633  lss0cl  19649  lssintcl  19667  lssincl  19668  reslmhm2  19756  lspvadd  19799  lspsntrim  19801  islbs3  19858  rrgeq0  19993  evlsval2  20230  cncrng  20496  xrsmcmn  20498  cndrng  20504  cnsrng  20509  xrs1mnd  20513  absabv  20532  psgnco  20657  zrhpsgninv  20659  zrhpsgnevpm  20665  zrhpsgnodpm  20666  zrhpsgnelbas  20668  zrhcopsgnelbas  20669  uvcresum  20867  lindfmm  20901  lindsmm  20902  mamudm  20929  mamufacex  20930  matsubgcell  20973  matsc  20989  scmatscmide  21046  scmatrhmcl  21067  1marepvsma1  21122  m1detdiag  21136  mdetralt  21147  m2detleiblem7  21166  gsummatr01lem3  21196  gsummatr01  21198  smadiadetlem0  21200  decpmate  21304  decpmatcl  21305  pm2mpcl  21335  pm2mpghmlem2  21350  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulgsum  21402  unopn  21441  clsss  21592  cldmre  21616  toponmre  21631  opnssneib  21653  restabs  21703  restcls  21719  restntr  21720  hausnei2  21891  cmpsublem  21937  bwth  21948  hausmapdom  22038  ptpjcn  22149  upxp  22161  ptrescn  22177  xkopjcn  22194  fbssfi  22375  snfil  22402  ufprim  22447  rnelfm  22491  flimrest  22521  fclsrest  22562  tmdgsum  22633  blpnfctr  22975  mscl  23000  xmscl  23001  xmsge0  23002  xmseq0  23003  restmetu  23109  ngpds  23142  tngngp3  23194  unitnmn0  23206  xrsxmet  23346  metds0  23387  cncfmptc  23448  isclmp  23630  cnlmod  23673  ncvsi  23684  cphsqrtcl  23717  cfil3i  23801  cfilres  23828  cmssmscld  23882  cmmbl  24064  voliunlem2  24081  itg2ub  24263  itgrecl  24327  tdeglem3  24582  r1pid  24682  eflogeq  25112  cxpadd  25189  cxpcom  25247  logbchbase  25276  relogbreexp  25280  relogbzexp  25281  relogbmulexp  25283  logbleb  25288  logblt  25289  lawcos  25321  pythag  25322  asinsinb  25402  acoscosb  25403  atantanb  25429  amgmlem  25495  lgsneg  25825  lgsne0  25839  lgsmodeq  25846  lgsmulsqcoprm  25847  gausslemma2dlem1a  25869  2sqreulem2  25956  brbtwn2  26619  colinearalg  26624  eleesubd  26626  axcgrrflx  26628  axcgrtr  26629  axsegcon  26641  ax5seglem1  26642  ax5seglem2  26643  ax5seglem4  26646  axbtwnid  26653  axlowdimlem14  26669  axlowdim  26675  axcontlem5  26682  axcontlem7  26684  nb3grprlem2  27091  cplgr3v  27145  cusgrsizeindslem  27161  sizusglecusglem2  27172  umgr2v2e  27235  cusgrrusgr  27291  iswlk  27320  edginwlk  27344  uspgr2wlkeq  27355  uspgr2wlkeq2  27356  uspgr2wlkeqi  27357  wlkonprop  27368  wlkon2n0  27376  pthdadjvtx  27439  upgr2pthnlp  27441  spthonepeq  27461  pthdlem2lem  27476  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  wlkiswwlks2lem4  27578  wlkiswwlks2lem6  27580  wlklnwwlkln2lem  27588  wwlksnred  27598  wwlksnextbi  27600  wwlksnextwrd  27603  2pthdlem1  27637  2wlkdlem10  27642  umgr2adedgwlkonALT  27654  elwwlks2s3  27658  elwwlks2ons3im  27661  s3wwlks2on  27663  2wspdisj  27669  2wspiundisj  27670  clwwlkgt0  27692  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlk  27708  clwlkclwwlk2  27709  clwlkclwwlkfo  27715  clwwisshclwwslemlem  27719  erclwwlktr  27728  clwwlkf  27754  wwlksubclwwlk  27765  erclwwlkntr  27778  clwwlknon  27797  frcond1  27973  frgr3v  27982  3vfriswmgr  27985  frgrwopreglem4a  28017  frrusgrord0lem  28046  clwwnonrepclwwnon  28052  extwwlkfab  28059  numclwwlk1lem2f1  28064  numclwwlk1lem2fo  28065  clwlknon2num  28075  numclwwlk2lem1  28083  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  numclwwlk2  28088  frgrreggt1  28100  friendshipgt3  28105  imsmetlem  28395  nmoxr  28471  nmoolb  28476  blometi  28508  phpar2  28528  phpar  28529  ipasslem5  28540  hvadd32  28739  hvaddsub12  28743  hvaddsubass  28746  hvsubass  28749  hvsub32  28750  hvsubdistr1  28754  hvsubdistr2  28755  hvmulcan  28777  hvmulcan2  28778  hvsubcan  28779  his5  28791  his2sub  28797  hhssabloilem  28966  hhssnv  28969  shlej2  29066  pjoi0  29422  hodcl  29452  hoadd32  29488  hosubdi  29513  hosubsub2  29517  hoaddsubass  29520  hosubsub4  29523  nmoplb  29612  unop  29620  hmop  29627  nmfnlb  29629  lnopmul  29672  kbass1  29821  kbass2  29822  leopmul2i  29840  leoptr  29842  cvntr  29997  mdslmd4i  30038  mdexchi  30040  atcv1  30085  sumdmdii  30120  fcoinvbr  30287  fpwrelmapffs  30397  xreceu  30526  isinftm  30738  unitdivcld  31044  esummulc1  31240  hasheuni  31244  unelsiga  31293  inelpisys  31313  carsgsigalem  31473  signswmnd  31727  bnj545  32067  bnj594  32084  bnj1311  32194  hashf1dmcdm  32254  usgrgt2cycl  32275  subgrwlk  32277  acycgr1v  32294  cvmsf1o  32417  cvmscld  32418  satefvfmla1  32570  elnanelprv  32574  lediv2aALT  32818  gcd32  32881  fununiq  32910  trpredpo  32972  poseq  32993  frr3g  33019  sltres  33067  sltletr  33133  sletr  33135  nocvxmin  33146  dfrdg4  33310  brcolinear  33418  colinearex  33419  nn0prpwlem  33568  clsun  33574  fnemeet1  33612  fnemeet2  33613  fnejoin1  33614  fnejoin2  33615  eltail  33620  rdgeqoa  34534  nlpineqsn  34572  curf  34752  lindsadd  34767  poimirlem28  34802  cnambfre  34822  ftc1anclem4  34852  cocanfo  34876  f1ocan1fv  34884  metf1o  34913  ismtybnd  34968  ghomco  35052  isdrngo2  35119  inidl  35191  igenmin  35225  brxrn  35508  brredunds  35743  cmtvalN  36229  cvrval  36287  pmapmeet  36791  paddval  36816  paddssat  36832  elpcliN  36911  pclssN  36912  pclunN  36916  paddunN  36945  poldmj1N  36946  tendoplcl2  37796  tendoplcl  37799  dihmeet  38361  expgcd  39063  zexpgcd  39065  reltsub1  39096  reltsubadd2  39097  resubsub4  39099  reppncan  39103  resubdi  39106  readdcan2  39122  mapco2g  39191  mzpcompact2lem  39228  eqrabdioph  39254  lerabdioph  39282  eluzrabdioph  39283  ltrabdioph  39285  nerabdioph  39286  dvdsrabdioph  39287  reglogcl  39367  rmxyadd  39398  rmyabs  39435  congadd  39443  congabseq  39451  rmydioph  39491  mendring  39672  mendlmod  39673  iocinico  39698  relexp0a  39941  relexpaddss  39943  brcoffn  40260  dvconstbi  40546  uzwo4  41195  ssin0  41197  ssinc  41233  ssdec  41234  fvmpt2bd  41306  disjf1o  41332  ssnnf1octb  41336  sub31  41437  fperiodmullem  41450  ssfiunibd  41456  infxr  41515  fmul01  41741  islptre  41780  lptre2pt  41801  limcleqr  41805  limclner  41812  limsuppnflem  41871  limsupvaluz2  41899  supcnvlimsup  41901  xlimmnfvlem2  41994  xlimmnfv  41995  xlimpnfvlem2  41998  xlimpnfv  41999  climxlim2lem  42006  coskpi2  42027  cosknegpi  42030  dvnmptdivc  42103  dvdsn1add  42104  dvnmptconst  42106  dvmptfprod  42110  dvnprodlem1  42111  dvnprodlem2  42112  ovolsplit  42154  stoweidlem60  42226  stowei  42230  dirkeritg  42268  fourierdlem70  42342  fourierdlem71  42343  fourierdlem103  42375  fourierdlem104  42376  fouriersw  42397  rrxtopnfi  42453  saluncl  42483  salexct  42498  sge0ltfirp  42563  sge0iunmpt  42581  meadjiunlem  42628  meaiuninc3v  42647  carageniuncllem1  42684  caratheodorylem1  42689  ovncvrrp  42727  ovnsubaddlem1  42733  hspmbllem2  42790  ovolval5lem3  42817  smfpimbor1lem1  42954  smfsuplem1  42966  smflimsuplem4  42978  sigarls  42995  cnambpcma  43375  elfzelfzlble  43402  fzoopth  43408  m1mod0mod1  43410  fsumsplitsndif  43414  iccpartiltu  43429  prproropf1olem2  43513  fmtno4prmfac  43581  2pwp1prmfmtno  43599  lighneallem4b  43621  mogoldbblem  43732  gbegt5  43773  sbgoldbm  43796  nnsum3primesle9  43806  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  evengpoap3  43811  nnsum4primesevenALTV  43813  isomgrtr  43851  strisomgrop  43852  isupwlk  43858  lidldomnnring  44099  2zrngacmnd  44111  rhmsubclem2  44256  rhmsubcALTVlem2  44274  zlmodzxzscm  44303  gsumlsscl  44329  lincvalsng  44369  lincvalpr  44371  lincdifsn  44377  linc1  44378  lincellss  44379  difmodm1lt  44480  fdivmpt  44498  digexp  44565  line  44617  rrxline  44619  itsclc0xyqsolr  44654  amgmwlem  44801
  Copyright terms: Public domain W3C validator