Theorem ad4antr 744

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad4antr	⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 485	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 742	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad5antr  746  ad5antlr  747  simp-4l  794  tfrlem1  8350  prdsval  17496  catass  17730  catpropd  17753  cidpropd  17754  subccocl  17890  funcco  17916  natpropd  18024  fucpropd  18025  initoeu2lem1  18059  prfval  18243  xpcpropd  18252  acsfiindd  18597  chnind  18665  chnso  18668  mndpsuppss  18811  mhmmnd  19118  ghmqusnsg  19340  ghmquskerlem3  19344  ghmqusker  19345  omndmul2  20191  rhmpreimaidl  21375  rhmqusnsg  21384  isprmidlc  21431  qsidomlem1  21437  qsidomlem2  21438  ssdifidlprm  21443  mhpmulcl  22269  psdmul  22286  scmatscm  22627  cpmatmcllem  22832  mptcoe1matfsupp  22916  mp2pm2mplem4  22923  chpdmatlem2  22953  chfacfisf  22968  chfacfisfcpmat  22969  neitr  23294  hauscmplem  23520  trcfilu  24407  cfilucfil  24673  restmetu  24684  metucn  24685  cnheibor  25071  dvlip2  26111  lgamucov  27156  bdayfinbndlem1  28614  tgifscgr  28731  iscgrglt  28737  tgbtwnconn1  28798  legtrd  28812  legtri3  28813  legso  28822  hlcgrex  28839  tglndim0  28852  tglinethru  28859  tglinesseq  28863  colline  28873  tglnpt2  28876  tglnpt4  28878  perpneq  28941  isperp2  28942  footexALT  28945  opphllem  28962  midex  28964  opphllem3  28976  opphllem5  28978  opphllem6  28979  opphl  28981  outpasch  28982  hlpasch  28983  lnopp2hpgb  28990  hpgerlem  28992  lnincplng  29010  plngcplem  29011  plngrotlem1  29013  lnssplnglem  29017  lnssplng  29018  plng3p  29019  lmieu  29032  lnperpex  29051  trgcopy  29052  cgrahl  29075  acopy  29081  inaghl  29093  cgrg3col4  29101  f1otrg  29125  nbumgrvtx  29601  3cyclfrgr  30544  numclwlk2lem2f1o  30635  s3f1  33175  ccatws1f1o  33179  dfmgc2  33224  pwrssmgc  33228  mgcf1o  33231  mndlrinvb  33253  gsumwun  33304  psgnfzto1stlem  33328  cycpmrn  33371  tocyccntz  33372  cycpmconjs  33384  isarchi3  33415  archirngz  33417  elrgspnlem2  33471  elrgspnlem4  33473  elrgspnsubrunlem2  33476  erler  33493  rlocaddval  33497  rlocmulval  33498  rloccring  33499  rloc1r  33501  ricdomn1  33517  fracfld  33539  nsgqusf1olem1  33633  nsgqusf1olem2  33634  nsgqusf1olem3  33635  lmhmqusker  33637  rhmquskerlem  33644  elrspunidl  33647  elrspunsn  33648  idlinsubrg  33650  rhmimaidl  33651  drngidl  33652  mxidlprm  33665  mxidlirredi  33666  mxidlirred  33667  drngmxidlr  33672  opprqusplusg  33683  opprqusmulr  33685  qsdrngi  33689  qsdrng  33691  drnglring  33694  dflring2  33695  dflringlem2  33697  dflringlem3  33698  dflring3  33699  dflring4  33700  rsprprmprmidlb  33725  rprmirred  33733  rprmirredb  33734  rprmdvdsprod  33736  1arithidom  33739  pidufd  33745  1arithufdlem2  33747  1arithufdlem3  33748  1arithufdlem4  33749  dfufd2lem  33751  deg1prod  33785  mplidomlem  33829  mplmulmvr  33841  mplvrpmrhm  33849  psrgsum  33850  psrmonprod  33854  esplyfv  33872  esplyfval1  33875  esplyind  33877  dimkerim  33929  fedgmul  33933  extdg1id  33968  evls1fldgencl  33972  fldextrspunlsplem  33975  fldextrspunlsp  33976  extdgfialglem1  33994  extdgfialg  33996  minplyirred  34013  constrextdg2lem  34050  constrfiss  34053  cos9thpiminplylem2  34085  qtophaus  34138  zarclsint  34174  zarcmplem  34183  esumcst  34365  sigapildsys  34464  oms0  34599  omssubadd  34602  carsgclctunlem3  34622  eulerpartlemgvv  34678  signsply0  34850  signstfvneq0  34871  actfunsnf1o  34903  reprsuc  34914  reprinfz1  34921  breprexplema  34929  breprexplemc  34931  hgt750lemb  34955  cvmlift3lem2  35678  satfdmlem  35726  nn0prpwlem  36690  lindsenlbs  38121  matunitlindflem1  38122  mblfinlem3  38165  mblfinlem4  38166  itg2addnclem2  38178  itg2gt0cn  38181  ftc1cnnc  38198  ftc1anc  38207  sstotbnd2  38280  lcfl8  42133  aks4d1p8  42711  fldhmf1  42714  mndmolinv  42719  primrootsunit1  42721  primrootscoprmpow  42723  primrootspoweq0  42730  aks6d1c2p2  42743  aks6d1c2lem4  42751  aks6d1c6lem3  42796  aks6d1c7  42808  unitscyglem2  42820  aks5  42828  fiabv  43161  fsuppind  43179  prjspersym  43196  pell1234qrdich  43445  pell14qrdich  43453  pell1qrgap  43458  pellfundex  43470  omabs2  43916  cvgdvgrat  44882  infleinflem2  45945  xrralrecnnle  45957  climrec  46178  climsuse  46183  limcrecl  46204  limsupubuz  46286  limsupgtlem  46350  xlimliminflimsup  46435  fperdvper  46492  dvnprodlem2  46520  etransclem35  46842  hspmbllem2  47200  smflimlem2  47345  smflimlem4  47347  iccpartgt  48032  prproropf1olem4  48111  sfprmdvdsmersenne  48211  gricushgr  48538  2zlidl  48861  ply1mulgsumlem2  49019  nn0sumshdiglemA  49251  imaf1co  49785  uppropd  49811  fuco21  49966  functhinclem4  50077  2arwcat  50230