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  8387  prdsval  17632  catass  17866  catpropd  17889  cidpropd  17890  subccocl  18026  funcco  18052  natpropd  18160  fucpropd  18161  initoeu2lem1  18195  prfval  18379  xpcpropd  18388  acsfiindd  18733  chnind  18801  chnso  18804  mndpsuppss  18965  mhmmnd  19280  ghmqusnsg  19502  ghmquskerlem3  19506  ghmqusker  19507  omndmul2  20353  drngidl  21545  rhmpreimaidl  21577  rhmqusnsg  21587  isprmidlc  21634  qsidomlem1  21642  qsidomlem2  21643  ssdifidlprm  21648  lindsenlbs  22163  mhpmulcl  22476  psdmul  22493  scmatscm  22834  matunitlindflem1  23000  cpmatmcllem  23042  mptcoe1matfsupp  23126  mp2pm2mplem4  23133  chpdmatlem2  23163  chfacfisf  23178  chfacfisfcpmat  23179  neitr  23504  hauscmplem  23730  trcfilu  24618  cfilucfil  24884  restmetu  24895  metucn  24896  cnheibor  25282  dvlip2  26321  lgamucov  27371  bdayfinbndlem1  28859  tgifscgr  28977  iscgrglt  28983  tgbtwnconn1  29044  legtrd  29058  legtri3  29059  legso  29068  hlcgrex  29088  tglndim0  29103  tglinethru  29110  tglinesseq  29114  colline  29124  tglnpt2  29127  tglnpt4  29129  perpneq  29195  isperp2  29196  footexALT  29199  opphllem  29217  midex  29219  opphllem3  29231  opphllem5  29233  opphllem6  29234  opphl  29236  outpasch  29239  hlpasch  29240  lnopp2hpgb  29247  hpgerlem  29249  lnincplng  29268  plngcplem  29269  plngrotlem1  29271  lnssplnglem  29275  lnssplng  29276  plng3p  29281  lmieu  29295  lnperpex  29315  trgcopy  29317  cgrahl  29341  acopy  29347  tgaaddcpbl  29358  inaghl  29370  cgrg3col4  29378  cgrabasimass  29384  angmgmaddeu1  29385  angmgmaddeu2  29386  angmgmaddeu3  29387  angmgmaddcpbl  29396  angmgmaddcl  29397  angmgmaddrid  29399  prlnghpg  29430  dfprlng2  29431  dfprlng3  29432  perpprlng  29434  prlngex  29435  prlngmolem1  29436  prlngmolem2  29437  quadcgrprlng  29450  f1otrg  29454  nbumgrvtx  29933  3cyclfrgr  30895  numclwlk2lem2f1o  30986  s3f1  33558  ccatws1f1o  33561  dfmgc2  33604  pwrssmgc  33608  mgcf1o  33611  mndlrinvb  33633  gsumwun  33684  psgnfzto1stlem  33708  cycpmrn  33751  tocyccntz  33752  cycpmconjs  33764  isarchi3  33795  archirngz  33797  elrgspnlem2  33851  elrgspnlem4  33853  elrgspnsubrunlem2  33856  erler  33873  rlocaddval  33877  rlocmulval  33878  rloccring  33879  rloc1r  33881  ricdomn1  33897  fracfld  33917  nsgqusf1olem1  34011  nsgqusf1olem2  34012  nsgqusf1olem3  34013  lmhmqusker  34015  rhmquskerlem  34022  elrspunidl  34025  elrspunsn  34026  idlinsubrg  34028  rhmimaidl  34029  mxidlprm  34042  mxidlirredi  34043  mxidlirred  34044  drngmxidlr  34049  opprqusplusg  34060  opprqusmulr  34062  qsdrngi  34066  qsdrng  34068  drnglring  34071  dflring2  34072  dflringlem2  34074  dflringlem3  34075  dflring3  34076  dflring4  34077  rsprprmprmidlb  34102  rprmirred  34110  rprmirredb  34111  rprmdvdsprod  34113  1arithidom  34116  pidufd  34122  1arithufdlem2  34124  1arithufdlem3  34125  1arithufdlem4  34126  dfufd2lem  34128  deg1prod  34162  mplidomlem  34206  mplmulmvr  34218  mplvrpmrhm  34226  psrgsum  34227  psrmonprod  34231  esplyfv  34249  esplyfval1  34252  esplyind  34254  dimkerim  34306  fedgmul  34310  extdg1id  34345  evls1fldgencl  34349  fldextrspunlsplem  34352  fldextrspunlsp  34353  extdgfialglem1  34371  extdgfialg  34373  minplyirred  34390  constrextdg2lem  34427  constrfiss  34430  cos9thpiminplylem2  34462  qtophaus  34515  zarclsint  34551  zarcmplem  34560  esumcst  34742  sigapildsys  34842  oms0  34976  omssubadd  34979  carsgclctunlem3  34999  eulerpartlemgvv  35055  signsply0  35227  signstfvneq0  35248  actfunsnf1o  35280  reprsuc  35291  reprinfz1  35298  breprexplema  35306  breprexplemc  35308  hgt750lemb  35332  cvmlift3lem2  36172  satfdmlem  36220  nn0prpwlem  37203  mh-inf3f1  37422  mblfinlem3  38671  mblfinlem4  38672  itg2addnclem2  38684  itg2gt0cn  38687  ftc1cnnc  38704  ftc1anc  38713  sstotbnd2  38802  lcfl8  42653  aks4d1p8  43231  fldhmf1  43234  mndmolinv  43239  primrootsunit1  43241  primrootscoprmpow  43243  primrootspoweq0  43250  aks6d1c2p2  43263  aks6d1c2lem4  43271  aks6d1c6lem3  43316  aks6d1c7  43328  unitscyglem2  43340  aks5  43348  fiabv  43694  fsuppind  43712  prjspersym  43729  pell1234qrdich  43962  pell14qrdich  43970  pell1qrgap  43975  pellfundex  43987  omabs2  44428  cvgdvgrat  45391  infleinflem2  46476  xrralrecnnle  46488  climrec  46709  climsuse  46714  limcrecl  46735  limsupubuz  46817  limsupgtlem  46881  xlimliminflimsup  46966  fperdvper  47023  dvnprodlem2  47051  etransclem35  47373  hspmbllem2  47731  smflimlem2  47876  smflimlem4  47878  iccpartgt  48603  prproropf1olem4  48682  sfprmdvdsmersenne  48782  gricushgr  49109  2zlidl  49431  ply1mulgsumlem2  49593  nn0sumshdiglemA  49825  imaf1co  50365  uppropd  50391  fuco21  50552  functhinclem4  50676  2arwcat  50832