Theorem 3adant1 1130

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

Step	Hyp	Ref	Expression
1		3adant.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantll 714	. 2 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)
3	2	3impa 1109	1 ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3ad2ant2  1134  3ad2ant3  1135  3simpc  1150  eupickb  2635  spc3egv  3557  sbciegftOLD  3778  reuhyp  5365  predtrss  6280  onunel  6424  funopg  6526  funprg  6546  funtpg  6547  funcnvtp  6555  unima  6909  fvun1  6925  fnreseql  6993  xpprsng  7085  ftpg  7101  f1ounsn  7218  f13dfv  7220  f1ocoima  7249  f1ofvswap  7252  mpoeq3ia  7436  ordunel  7769  fex2  7878  funexw  7896  poxp  8070  poxp2  8085  poxp3  8092  poseq  8100  suppval1  8108  wfr3g  8261  smores3  8285  oaord  8474  oacan  8475  oaword  8476  omord  8495  omcan  8496  omwordri  8499  odi  8506  omass  8507  oeord  8516  oecan  8517  oewordri  8520  oeordsuc  8522  nnaord  8547  nnaordr  8548  nndi  8551  nnmass  8552  nnaword  8555  nnmord  8560  nnmwordri  8564  naddelim  8614  naddel1  8615  naddel2  8616  naddss1  8617  naddss2  8618  naddasslem2  8623  nadd32  8625  erov  8751  ecopovtrn  8757  ixpf  8858  f1oen4g  8901  f1dom4g  8902  mapxpen  9071  ssfi  9097  sbthfilem  9122  sbthfi  9123  onomeneq  9138  fimax2g  9186  unbnn  9196  funisfsupp  9270  inelfi  9321  elfiun  9333  sup0  9370  suppr  9375  infpr  9408  ttrclss  9629  frr3g  9668  r111  9687  dif1card  9920  ackbij1lem16  10144  cff1  10168  cfflb  10169  cfsmolem  10180  fin23lem34  10256  hsmexlem2  10337  axcc3  10348  domtriomlem  10352  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  konigthlem  10479  gchdomtri  10540  tskpr  10681  tskop  10682  tskuni  10694  tskun  10697  gruop  10716  gruun  10717  grudomon  10728  adderpqlem  10865  mulerpqlem  10866  addassnq  10869  mulassnq  10870  distrnq  10872  ltsonq  10880  ltanq  10882  ltmnq  10883  genpass  10920  distrlem1pr  10936  distrlem4pr  10937  ltsopr  10943  adddir  11123  axlttrn  11205  ltletr  11225  letr  11227  mul32  11299  mul31  11300  add32  11352  subsub23  11385  addsubass  11390  subcan2  11406  subsub2  11409  nppcan2  11412  sub32  11415  nnncan  11416  nnncan2  11418  pnpcan2  11421  subdi  11570  subdir  11571  receu  11782  mulcan1g  11790  mulcan2g  11791  divmul3  11801  divrec  11812  divrec2  11813  div11  11824  divsubdir  11835  subdivcomb2  11837  divdiv1  11852  redivcl  11860  div2neg  11864  ltmul2  11992  lemul1  11993  lemul2  11994  lemul2a  11996  lediv1  12007  gt0div  12008  ge0div  12009  mulsuble0b  12014  ltdivmul  12017  ledivmul  12018  ltdivmul2  12019  ledivmul2  12021  lemuldiv  12022  ltdiv23  12033  lediv23  12034  ledivp1i  12067  ltdivp1i  12068  uzind2  12585  nn0ind  12587  fnn0ind  12591  uz3m2nn  12807  xrltletr  13071  xrletr  13072  xrre2  13085  xrltmin  13097  xrlemin  13099  xleadd2a  13169  xleadd1  13170  xltadd2  13172  xmulasslem3  13201  xmulass  13202  xltmul2  13208  ixxdisj  13276  iooneg  13387  iccneg  13388  icoshft  13389  icoshftf1o  13390  icodisj  13392  snunioo  13394  fzen  13457  ssfzunsnext  13485  fzrev3  13506  2ffzeq  13565  fzoaddel2  13636  elfzodifsumelfzo  13647  ssfzoulel  13676  ssfzo12bi  13677  fzoopth  13678  fzoshftral  13703  adddivflid  13738  flltdivnn0lt  13753  ltdifltdiv  13754  fldiv4p1lem1div2  13755  modcyc  13826  modcyc2  13827  modaddabs  13831  muladdmod  13835  modsubmodmod  13853  modaddmodup  13857  modaddmulmod  13861  moddi  13862  modsubdir  13863  expdiv  14036  digit2  14159  nfile  14282  hashdifpr  14338  hashgt23el  14347  hashreshashfun  14362  hashf1dmcdm  14367  hash3tpexb  14417  fi1uzind  14430  ccatval1  14500  ccatass  14512  swrdval  14567  swrdnd  14578  swrd0  14582  swrdfv2  14585  pfxsuff1eqwrdeq  14622  swrdswrdlem  14627  pfxccatin12lem2a  14650  pfxccatin12lem1  14651  repswccat  14709  cshwidxmod  14726  cshwidxmodr  14727  cshf1  14733  repswcshw  14735  2cshw  14736  2cshwcom  14739  2cshwcshw  14748  cshwcsh2id  14751  ccatco  14758  2swrd2eqwrdeq  14876  wwlktovf  14879  brcnvtrclfv  14926  shftval2  14998  mulre  15044  absdiv  15218  absdiflt  15241  absdifle  15242  abs3dif  15255  cau3  15279  ello12r  15440  elo12r  15451  modfsummods  15716  geoisum1c  15803  rpnnen2lem4  16142  rpnnen2lem7  16145  addmulmodb  16192  dvdsmulc  16210  dvdsmulcr  16212  dvdsmultr1  16223  dvdsmultr2  16225  dvdssub2  16228  oexpneg  16272  divalgb  16331  ndvdsadd  16337  sadass  16398  modgcd  16459  dvdsgcd  16471  dvdsgcdb  16472  gcdass  16474  mulgcd  16475  absmulgcd  16476  rpmulgcd  16484  expgcd  16490  zexpgcd  16492  nn0seqcvgd  16497  algcvga  16506  lcmdvdsb  16540  lcmass  16541  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  coprmdvds  16580  coprmdvds2  16581  rpmul  16586  cncongr1  16594  cncongr2  16595  qnumdenbi  16671  modprm0  16733  coprimeprodsq  16736  pythagtriplem4  16747  pythagtriplem8  16751  pythagtriplem9  16752  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem16  16758  pcpremul  16771  pcgcd  16806  vdwapval  16901  vdwapun  16902  prmgaplem3  16981  prmgaplem4  16982  prmgaplem7  16985  prmgapprmolem  16989  mreiincl  17515  mreincl  17518  mremre  17523  mrcss  17539  catcisolem  18034  pleval2  18258  pospo  18266  latlem  18360  latjcom  18370  latmcom  18386  lubss  18436  lubun  18438  clatglbss  18442  ipole  18457  ipolt  18458  pslem  18495  dirtr  18525  gsumsgrpccat  18765  gsumws2  18767  frmdmnd  18784  symggrplem  18809  isgrpi  18889  grpsubrcan  18951  grpinvsub  18952  grpsubeq0  18956  grpsubadd0sub  18957  grpnpcan  18962  qussub  19120  ghmsub  19153  symgpssefmnd  19325  symggrp  19329  symgextsymg  19353  gsmsymgreqlem2  19360  symgfixfolem1  19367  pmtrprfv3  19383  symggen  19399  lsmass  19598  efgsrel  19663  cntzcmn  19769  dvrcl  20340  unitdvcl  20341  dvrcan1  20345  subrngmre  20495  subrgmre  20530  rhmsubclem2  20619  rrgeq0  20633  abvsubtri  20760  abvtrivd  20765  lmodvsubval2  20868  rmodislmodlem  20880  rmodislmod  20881  lss0cl  20898  lssintcl  20915  lssincl  20916  reslmhm2  21005  lspvadd  21048  lspsntrim  21050  islbs3  21110  rnglidlmmgm  21200  cncrng  21343  cncrngOLD  21344  xrsmcmn  21346  cndrng  21353  cndrngOLD  21354  cnsrng  21360  absabv  21379  xrs1mnd  21395  psgnco  21538  zrhpsgninv  21540  zrhpsgnevpm  21546  zrhpsgnodpm  21547  zrhpsgnelbas  21549  zrhcopsgnelbas  21550  uvcresum  21748  lindfmm  21782  lindsmm  21783  evlsval2  22042  mamudm  22339  mamufacex  22340  matsubgcell  22378  matsc  22394  scmatscmide  22451  scmatrhmcl  22472  1marepvsma1  22527  m1detdiag  22541  mdetralt  22552  m2detleiblem7  22571  gsummatr01lem3  22601  gsummatr01  22603  smadiadetlem0  22605  decpmate  22710  decpmatcl  22711  pm2mpcl  22741  pm2mpghmlem2  22756  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  unopn  22847  clsss  22998  cldmre  23022  toponmre  23037  opnssneib  23059  restabs  23109  restcls  23125  restntr  23126  hausnei2  23297  cmpsublem  23343  bwth  23354  hausmapdom  23444  ptpjcn  23555  upxp  23567  ptrescn  23583  xkopjcn  23600  fbssfi  23781  snfil  23808  ufprim  23853  rnelfm  23897  flimrest  23927  fclsrest  23968  tmdgsum  24039  blpnfctr  24380  mscl  24405  xmscl  24406  xmsge0  24407  xmseq0  24408  restmetu  24514  ngpds  24548  tngngp3  24600  unitnmn0  24612  xrsxmet  24754  metds0  24795  mpomulcn  24814  cncfmptc  24861  isclmp  25053  cnlmod  25096  ncvsi  25107  cphsqrtcl  25140  cfil3i  25225  cfilres  25252  cmssmscld  25306  cmmbl  25491  voliunlem2  25508  itg2ub  25690  itgrecl  25755  r1pid  26122  eflogeq  26567  cxpadd  26644  cxpcom  26704  logbchbase  26737  relogbreexp  26741  relogbzexp  26742  relogbmulexp  26744  logbleb  26749  logblt  26750  lawcos  26782  pythag  26783  asinsinb  26863  acoscosb  26864  atantanb  26890  amgmlem  26956  lgsneg  27288  lgsne0  27302  lgsmodeq  27309  lgsmulsqcoprm  27310  gausslemma2dlem1a  27332  2sqreulem2  27419  ltsres  27630  noetainflem1  27705  ltlestr  27728  lestr  27730  nocvxmin  27751  madebdaylemold  27894  lrrecpo  27937  ltadds2im  27982  leadds1im  27983  leadds2im  27984  leadds1  27985  leadds2  27986  ltadds1  27988  addscan2  27989  addscan1  27990  subadds  28066  ltsubs1  28072  divscl  28219  oncutlt  28260  zsoring  28405  expscllem  28426  brbtwn2  28978  colinearalg  28983  eleesubd  28985  axcgrrflx  28987  axcgrtr  28988  axsegcon  29000  ax5seglem1  29001  ax5seglem2  29002  ax5seglem4  29005  axbtwnid  29012  axlowdimlem14  29028  axlowdim  29034  axcontlem5  29041  axcontlem7  29043  nb3grprlem2  29454  cplgr3v  29508  cusgrsizeindslem  29525  sizusglecusglem2  29536  umgr2v2e  29599  cusgrrusgr  29655  iswlk  29684  edginwlk  29708  uspgr2wlkeq  29719  uspgr2wlkeq2  29720  uspgr2wlkeqi  29721  wlkonprop  29730  wlkon2n0  29738  pthdadjvtx  29801  upgr2pthnlp  29805  spthonepeq  29825  pthdlem2lem  29840  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  wlkiswwlks2lem4  29945  wlkiswwlks2lem6  29947  wlklnwwlkln2lem  29955  wwlksnred  29965  wwlksnextbi  29967  wwlksnextwrd  29970  2pthdlem1  30003  2wlkdlem10  30008  umgr2adedgwlkonALT  30020  elwwlks2s3  30024  elwwlks2ons3im  30027  s3wwlks2on  30029  sps3wwlks2on  30030  2wspdisj  30038  2wspiundisj  30039  clwwlkgt0  30061  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlk  30077  clwlkclwwlk2  30078  clwlkclwwlkfo  30084  clwwisshclwwslemlem  30088  erclwwlktr  30097  clwwlkf  30122  wwlksubclwwlk  30133  erclwwlkntr  30146  clwwlknon  30165  frcond1  30341  frgr3v  30350  3vfriswmgr  30353  frgrwopreglem4a  30385  frrusgrord0lem  30414  clwwnonrepclwwnon  30420  extwwlkfab  30427  numclwwlk1lem2f1  30432  numclwwlk1lem2fo  30433  clwlknon2num  30443  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  numclwwlk2  30456  frgrreggt1  30468  friendshipgt3  30473  imsmetlem  30765  nmoxr  30841  nmoolb  30846  blometi  30878  phpar2  30898  phpar  30899  ipasslem5  30910  hvadd32  31109  hvaddsub12  31113  hvaddsubass  31116  hvsubass  31119  hvsub32  31120  hvsubdistr1  31124  hvsubdistr2  31125  hvmulcan  31147  hvmulcan2  31148  hvsubcan  31149  his5  31161  his2sub  31167  hhssabloilem  31336  hhssnv  31339  shlej2  31436  pjoi0  31792  hodcl  31822  hoadd32  31858  hosubdi  31883  hosubsub2  31887  hoaddsubass  31890  hosubsub4  31893  nmoplb  31982  unop  31990  hmop  31997  nmfnlb  31999  lnopmul  32042  kbass1  32191  kbass2  32192  leopmul2i  32210  leoptr  32212  cvntr  32367  mdslmd4i  32408  mdexchi  32410  atcv1  32455  sumdmdii  32490  fcoinvbr  32680  fpwrelmapffs  32813  xreceu  33003  isinftm  33263  unitdivcld  34058  esummulc1  34238  hasheuni  34242  unelsiga  34291  inelpisys  34311  carsgsigalem  34472  signswmnd  34714  bnj545  35051  bnj594  35068  bnj1311  35180  fissorduni  35246  r1filimi  35259  fineqvac  35272  fineqvnttrclselem3  35279  fineqvinfep  35281  usgrgt2cycl  35324  subgrwlk  35326  acycgr1v  35343  cvmsf1o  35466  cvmscld  35467  satefvfmla1  35619  elnanelprv  35623  lediv2aALT  35871  gcd32  35943  fununiq  35963  dfrdg4  36145  brcolinear  36253  colinearex  36254  nn0prpwlem  36516  clsun  36522  fnemeet1  36560  fnemeet2  36561  fnejoin1  36562  fnejoin2  36563  eltail  36568  rdgeqoa  37575  nlpineqsn  37613  curf  37799  lindsadd  37814  poimirlem28  37849  cnambfre  37869  ftc1anclem4  37897  cocanfo  37920  f1ocan1fv  37927  metf1o  37956  ismtybnd  38008  ghomco  38092  isdrngo2  38159  inidl  38231  igenmin  38265  brxrn  38568  brredunds  38883  cmtvalN  39471  cvrval  39529  pmapmeet  40033  paddval  40058  paddssat  40074  elpcliN  40153  pclssN  40154  pclunN  40158  paddunN  40187  poldmj1N  40188  tendoplcl2  41038  tendoplcl  41041  dihmeet  41603  lcmineqlem1  42283  reltsub1  42641  reltsubadd2  42642  resubsub4  42644  reppncan  42648  resubdi  42651  readdcan2  42668  subresre  42686  mapco2g  42956  mzpcompact2lem  42993  eqrabdioph  43019  lerabdioph  43047  eluzrabdioph  43048  ltrabdioph  43050  nerabdioph  43051  dvdsrabdioph  43052  reglogcl  43132  rmxyadd  43163  rmyabs  43200  congadd  43208  congabseq  43216  rmydioph  43256  mendring  43430  mendlmod  43431  iocinico  43454  omge1  43539  relexp0a  43957  relexpaddss  43959  brcoffn  44271  ismnushort  44542  dvconstbi  44575  uzwo4  45298  ssin0  45300  ssinc  45331  ssdec  45332  fvmpt2bd  45414  disjf1o  45435  ssnnf1octb  45438  sub31  45538  fperiodmullem  45551  ssfiunibd  45557  infxr  45611  fmul01  45826  islptre  45865  lptre2pt  45884  limcleqr  45888  limclner  45895  limsuppnflem  45954  limsupvaluz2  45982  supcnvlimsup  45984  xlimmnfvlem2  46077  xlimmnfv  46078  xlimpnfvlem2  46081  xlimpnfv  46082  climxlim2lem  46089  coskpi2  46110  cosknegpi  46113  dvnmptdivc  46182  dvdsn1add  46183  dvnmptconst  46185  dvmptfprod  46189  dvnprodlem1  46190  dvnprodlem2  46191  ovolsplit  46232  stoweidlem60  46304  stowei  46308  dirkeritg  46346  fourierdlem70  46420  fourierdlem71  46421  fourierdlem103  46453  fourierdlem104  46454  fouriersw  46475  rrxtopnfi  46531  saluncl  46561  salexct  46578  sge0ltfirp  46644  sge0iunmpt  46662  meadjiunlem  46709  meaiuninc3v  46728  carageniuncllem1  46765  caratheodorylem1  46770  ovncvrrp  46808  ovnsubaddlem1  46814  hspmbllem2  46871  ovolval5lem3  46898  smfpimbor1lem1  47042  smfsuplem1  47055  smflimsuplem4  47067  sigarls  47101  cnambpcma  47540  elfzelfzlble  47567  submodaddmod  47587  difltmodne  47588  m1mod0mod1  47600  modmkpkne  47607  mod2addne  47610  modm2nep1  47612  modm1nep2  47614  modm1nem2  47615  fsumsplitsndif  47619  fundcmpsurinjALT  47658  iccpartiltu  47668  prproropf1olem2  47750  fmtno4prmfac  47818  2pwp1prmfmtno  47836  lighneallem4b  47855  mogoldbblem  47966  gbegt5  48007  sbgoldbm  48030  nnsum3primesle9  48040  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  evengpoap3  48045  nnsum4primesevenALTV  48047  clnbgredg  48086  opstrgric  48172  clnbgrgrimlem  48179  grtrif1o  48188  isubgr3stgrlem1  48212  isubgr3stgrlem4  48215  gpgusgralem  48302  gpg3nbgrvtx0  48322  isupwlk  48382  lidldomnnring  48482  2zrngacmnd  48494  rhmsubcALTVlem2  48528  fprmappr  48591  zlmodzxzscm  48603  gsumlsscl  48626  lincvalsng  48662  lincvalpr  48664  lincdifsn  48670  linc1  48671  lincellss  48672  fdivmpt  48786  digexp  48853  2arymaptfo  48900  line  48978  rrxline  48980  itsclc0xyqsolr  49015  iscnrm3r  49193  resipos  49220  amgmwlem  50047