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  8367  prdsval  17606  catass  17840  catpropd  17863  cidpropd  17864  subccocl  18000  funcco  18026  natpropd  18134  fucpropd  18135  initoeu2lem1  18169  prfval  18353  xpcpropd  18362  acsfiindd  18707  chnind  18775  chnso  18778  mndpsuppss  18939  mhmmnd  19254  ghmqusnsg  19476  ghmquskerlem3  19480  ghmqusker  19481  omndmul2  20327  drngidl  21519  rhmpreimaidl  21551  rhmqusnsg  21561  isprmidlc  21608  qsidomlem1  21616  qsidomlem2  21617  ssdifidlprm  21622  lindsenlbs  22137  mhpmulcl  22450  psdmul  22467  scmatscm  22808  matunitlindflem1  22974  cpmatmcllem  23016  mptcoe1matfsupp  23100  mp2pm2mplem4  23107  chpdmatlem2  23137  chfacfisf  23152  chfacfisfcpmat  23153  neitr  23478  hauscmplem  23704  trcfilu  24592  cfilucfil  24858  restmetu  24869  metucn  24870  cnheibor  25256  dvlip2  26295  lgamucov  27347  bdayfinbndlem1  28835  tgifscgr  28953  iscgrglt  28959  tgbtwnconn1  29020  legtrd  29034  legtri3  29035  legso  29044  hlcgrex  29064  tglndim0  29079  tglinethru  29086  tglinesseq  29090  colline  29100  tglnpt2  29103  tglnpt4  29105  perpneq  29171  isperp2  29172  footexALT  29175  opphllem  29193  midex  29195  opphllem3  29207  opphllem5  29209  opphllem6  29210  opphl  29212  outpasch  29215  hlpasch  29216  lnopp2hpgb  29223  hpgerlem  29225  lnincplng  29244  plngcplem  29245  plngrotlem1  29247  lnssplnglem  29251  lnssplng  29252  plng3p  29257  lmieu  29271  lnperpex  29291  trgcopy  29293  cgrahl  29317  acopy  29323  tgaaddcpbl  29334  inaghl  29346  cgrg3col4  29354  cgrabasimass  29360  angmgmaddeu1  29361  angmgmaddeu2  29362  angmgmaddeu3  29363  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddrid  29375  prlnghpg  29406  dfprlng2  29407  dfprlng3  29408  perpprlng  29410  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  quadcgrprlng  29426  f1otrg  29430  nbumgrvtx  29909  3cyclfrgr  30871  numclwlk2lem2f1o  30962  s3f1  33493  ccatws1f1o  33496  dfmgc2  33539  pwrssmgc  33543  mgcf1o  33546  mndlrinvb  33568  gsumwun  33619  psgnfzto1stlem  33643  cycpmrn  33686  tocyccntz  33687  cycpmconjs  33699  isarchi3  33730  archirngz  33732  elrgspnlem2  33786  elrgspnlem4  33788  elrgspnsubrunlem2  33791  erler  33808  rlocaddval  33812  rlocmulval  33813  rloccring  33814  rloc1r  33816  ricdomn1  33832  fracfld  33852  nsgqusf1olem1  33946  nsgqusf1olem2  33947  nsgqusf1olem3  33948  lmhmqusker  33950  rhmquskerlem  33957  elrspunidl  33960  elrspunsn  33961  idlinsubrg  33963  rhmimaidl  33964  mxidlprm  33977  mxidlirredi  33978  mxidlirred  33979  drngmxidlr  33984  opprqusplusg  33995  opprqusmulr  33997  qsdrngi  34001  qsdrng  34003  drnglring  34006  dflring2  34007  dflringlem2  34009  dflringlem3  34010  dflring3  34011  dflring4  34012  rsprprmprmidlb  34037  rprmirred  34045  rprmirredb  34046  rprmdvdsprod  34048  1arithidom  34051  pidufd  34057  1arithufdlem2  34059  1arithufdlem3  34060  1arithufdlem4  34061  dfufd2lem  34063  deg1prod  34097  mplidomlem  34141  mplmulmvr  34153  mplvrpmrhm  34161  psrgsum  34162  psrmonprod  34166  esplyfv  34184  esplyfval1  34187  esplyind  34189  dimkerim  34241  fedgmul  34245  extdg1id  34280  evls1fldgencl  34284  fldextrspunlsplem  34287  fldextrspunlsp  34288  extdgfialglem1  34306  extdgfialg  34308  minplyirred  34325  constrextdg2lem  34362  constrfiss  34365  cos9thpiminplylem2  34397  qtophaus  34450  zarclsint  34486  zarcmplem  34495  esumcst  34677  sigapildsys  34777  oms0  34912  omssubadd  34915  carsgclctunlem3  34935  eulerpartlemgvv  34991  signsply0  35163  signstfvneq0  35184  actfunsnf1o  35216  reprsuc  35227  reprinfz1  35234  breprexplema  35242  breprexplemc  35244  hgt750lemb  35268  cvmlift3lem2  36054  satfdmlem  36102  nn0prpwlem  37080  mh-inf3f1  37299  mblfinlem3  38545  mblfinlem4  38546  itg2addnclem2  38558  itg2gt0cn  38561  ftc1cnnc  38578  ftc1anc  38587  sstotbnd2  38676  lcfl8  42527  aks4d1p8  43105  fldhmf1  43108  mndmolinv  43113  primrootsunit1  43115  primrootscoprmpow  43117  primrootspoweq0  43124  aks6d1c2p2  43137  aks6d1c2lem4  43145  aks6d1c6lem3  43190  aks6d1c7  43202  unitscyglem2  43214  aks5  43222  fiabv  43562  fsuppind  43580  prjspersym  43597  pell1234qrdich  43821  pell14qrdich  43829  pell1qrgap  43834  pellfundex  43846  omabs2  44292  cvgdvgrat  45256  infleinflem2  46326  xrralrecnnle  46338  climrec  46559  climsuse  46564  limcrecl  46585  limsupubuz  46667  limsupgtlem  46731  xlimliminflimsup  46816  fperdvper  46873  dvnprodlem2  46901  etransclem35  47223  hspmbllem2  47581  smflimlem2  47726  smflimlem4  47728  iccpartgt  48453  prproropf1olem4  48532  sfprmdvdsmersenne  48632  gricushgr  48959  2zlidl  49281  ply1mulgsumlem2  49443  nn0sumshdiglemA  49675  imaf1co  50207  uppropd  50233  fuco21  50388  functhinclem4  50499  2arwcat  50652