Theorem ad4antr 745

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 486	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 743	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5antr  747  ad5antlr  748  simp-4l  795  tfrlem1  8371  prdsval  17533  catass  17767  catpropd  17790  cidpropd  17791  subccocl  17927  funcco  17953  natpropd  18061  fucpropd  18062  initoeu2lem1  18096  prfval  18280  xpcpropd  18289  acsfiindd  18634  chnind  18702  chnso  18705  mndpsuppss  18854  mhmmnd  19161  ghmqusnsg  19383  ghmquskerlem3  19387  ghmqusker  19388  omndmul2  20234  drngidl  21422  rhmpreimaidl  21453  rhmqusnsg  21462  isprmidlc  21509  qsidomlem1  21517  qsidomlem2  21518  ssdifidlprm  21523  mhpmulcl  22349  psdmul  22366  scmatscm  22707  cpmatmcllem  22912  mptcoe1matfsupp  22996  mp2pm2mplem4  23003  chpdmatlem2  23033  chfacfisf  23048  chfacfisfcpmat  23049  neitr  23374  hauscmplem  23600  trcfilu  24487  cfilucfil  24753  restmetu  24764  metucn  24765  cnheibor  25151  dvlip2  26191  lgamucov  27239  bdayfinbndlem1  28697  tgifscgr  28814  iscgrglt  28820  tgbtwnconn1  28881  legtrd  28895  legtri3  28896  legso  28905  hlcgrex  28925  tglndim0  28939  tglinethru  28946  tglinesseq  28950  colline  28960  tglnpt2  28963  tglnpt4  28965  perpneq  29031  isperp2  29032  footexALT  29035  opphllem  29053  midex  29055  opphllem3  29067  opphllem5  29069  opphllem6  29070  opphl  29072  outpasch  29074  hlpasch  29075  lnopp2hpgb  29082  hpgerlem  29084  lnincplng  29103  plngcplem  29104  plngrotlem1  29106  lnssplnglem  29110  lnssplng  29111  plng3p  29116  lmieu  29130  lnperpex  29150  trgcopy  29152  cgrahl  29175  acopy  29181  inaghl  29199  cgrg3col4  29207  prlnghpg  29233  dfprlng2  29234  dfprlng3  29235  perpprlng  29237  prlngex  29238  prlngmolem1  29239  prlngmolem2  29240  quadcgrprlng  29253  f1otrg  29257  nbumgrvtx  29733  3cyclfrgr  30676  numclwlk2lem2f1o  30767  s3f1  33301  ccatws1f1o  33304  dfmgc2  33347  pwrssmgc  33351  mgcf1o  33354  mndlrinvb  33376  gsumwun  33427  psgnfzto1stlem  33451  cycpmrn  33494  tocyccntz  33495  cycpmconjs  33507  isarchi3  33538  archirngz  33540  elrgspnlem2  33594  elrgspnlem4  33596  elrgspnsubrunlem2  33599  erler  33616  rlocaddval  33620  rlocmulval  33621  rloccring  33622  rloc1r  33624  ricdomn1  33640  fracfld  33660  nsgqusf1olem1  33753  nsgqusf1olem2  33754  nsgqusf1olem3  33755  lmhmqusker  33757  rhmquskerlem  33764  elrspunidl  33767  elrspunsn  33768  idlinsubrg  33770  rhmimaidl  33771  mxidlprm  33784  mxidlirredi  33785  mxidlirred  33786  drngmxidlr  33791  opprqusplusg  33802  opprqusmulr  33804  qsdrngi  33808  qsdrng  33810  drnglring  33813  dflring2  33814  dflringlem2  33816  dflringlem3  33817  dflring3  33818  dflring4  33819  rsprprmprmidlb  33844  rprmirred  33852  rprmirredb  33853  rprmdvdsprod  33855  1arithidom  33858  pidufd  33864  1arithufdlem2  33866  1arithufdlem3  33867  1arithufdlem4  33868  dfufd2lem  33870  deg1prod  33904  mplidomlem  33948  mplmulmvr  33960  mplvrpmrhm  33968  psrgsum  33969  psrmonprod  33973  esplyfv  33991  esplyfval1  33994  esplyind  33996  dimkerim  34048  fedgmul  34052  extdg1id  34087  evls1fldgencl  34091  fldextrspunlsplem  34094  fldextrspunlsp  34095  extdgfialglem1  34113  extdgfialg  34115  minplyirred  34132  constrextdg2lem  34169  constrfiss  34172  cos9thpiminplylem2  34204  qtophaus  34257  zarclsint  34293  zarcmplem  34302  esumcst  34484  sigapildsys  34584  oms0  34719  omssubadd  34722  carsgclctunlem3  34742  eulerpartlemgvv  34798  signsply0  34970  signstfvneq0  34991  actfunsnf1o  35023  reprsuc  35034  reprinfz1  35041  breprexplema  35049  breprexplemc  35051  hgt750lemb  35075  cvmlift3lem2  35833  satfdmlem  35881  nn0prpwlem  36874  lindsenlbs  38307  matunitlindflem1  38308  mblfinlem3  38351  mblfinlem4  38352  itg2addnclem2  38364  itg2gt0cn  38367  ftc1cnnc  38384  ftc1anc  38393  sstotbnd2  38466  lcfl8  42317  aks4d1p8  42895  fldhmf1  42898  mndmolinv  42903  primrootsunit1  42905  primrootscoprmpow  42907  primrootspoweq0  42914  aks6d1c2p2  42927  aks6d1c2lem4  42935  aks6d1c6lem3  42980  aks6d1c7  42992  unitscyglem2  43004  aks5  43012  fiabv  43345  fsuppind  43363  prjspersym  43380  pell1234qrdich  43629  pell14qrdich  43637  pell1qrgap  43642  pellfundex  43654  omabs2  44100  cvgdvgrat  45064  infleinflem2  46127  xrralrecnnle  46139  climrec  46360  climsuse  46365  limcrecl  46386  limsupubuz  46468  limsupgtlem  46532  xlimliminflimsup  46617  fperdvper  46674  dvnprodlem2  46702  etransclem35  47024  hspmbllem2  47382  smflimlem2  47527  smflimlem4  47529  iccpartgt  48217  prproropf1olem4  48296  sfprmdvdsmersenne  48396  gricushgr  48723  2zlidl  49046  ply1mulgsumlem2  49208  nn0sumshdiglemA  49440  imaf1co  49974  uppropd  50000  fuco21  50155  functhinclem4  50266  2arwcat  50419