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  8364  prdsval  17540  catass  17774  catpropd  17797  cidpropd  17798  subccocl  17934  funcco  17960  natpropd  18068  fucpropd  18069  initoeu2lem1  18103  prfval  18287  xpcpropd  18296  acsfiindd  18641  chnind  18709  chnso  18712  mndpsuppss  18872  mhmmnd  19187  ghmqusnsg  19409  ghmquskerlem3  19413  ghmqusker  19414  omndmul2  20260  drngidl  21448  rhmpreimaidl  21479  rhmqusnsg  21488  isprmidlc  21535  qsidomlem1  21543  qsidomlem2  21544  ssdifidlprm  21549  lindsenlbs  22064  mhpmulcl  22377  psdmul  22394  scmatscm  22735  matunitlindflem1  22901  cpmatmcllem  22943  mptcoe1matfsupp  23027  mp2pm2mplem4  23034  chpdmatlem2  23064  chfacfisf  23079  chfacfisfcpmat  23080  neitr  23405  hauscmplem  23631  trcfilu  24519  cfilucfil  24785  restmetu  24796  metucn  24797  cnheibor  25183  dvlip2  26222  lgamucov  27274  bdayfinbndlem1  28732  tgifscgr  28850  iscgrglt  28856  tgbtwnconn1  28917  legtrd  28931  legtri3  28932  legso  28941  hlcgrex  28961  tglndim0  28976  tglinethru  28983  tglinesseq  28987  colline  28997  tglnpt2  29000  tglnpt4  29002  perpneq  29068  isperp2  29069  footexALT  29072  opphllem  29090  midex  29092  opphllem3  29104  opphllem5  29106  opphllem6  29107  opphl  29109  outpasch  29112  hlpasch  29113  lnopp2hpgb  29120  hpgerlem  29122  lnincplng  29141  plngcplem  29142  plngrotlem1  29144  lnssplnglem  29148  lnssplng  29149  plng3p  29154  lmieu  29168  lnperpex  29188  trgcopy  29190  cgrahl  29214  acopy  29220  tgaaddcpbl  29231  inaghl  29243  cgrg3col4  29251  cgrabasimass  29257  angmgmaddeu1  29258  angmgmaddeu2  29259  angmgmaddeu3  29260  angmgmaddcpbl  29269  angmgmaddcl  29270  angmgmaddrid  29272  prlnghpg  29303  dfprlng2  29304  dfprlng3  29305  perpprlng  29307  prlngex  29308  prlngmolem1  29309  prlngmolem2  29310  quadcgrprlng  29323  f1otrg  29327  nbumgrvtx  29806  3cyclfrgr  30768  numclwlk2lem2f1o  30859  s3f1  33390  ccatws1f1o  33393  dfmgc2  33436  pwrssmgc  33440  mgcf1o  33443  mndlrinvb  33465  gsumwun  33516  psgnfzto1stlem  33540  cycpmrn  33583  tocyccntz  33584  cycpmconjs  33596  isarchi3  33627  archirngz  33629  elrgspnlem2  33683  elrgspnlem4  33685  elrgspnsubrunlem2  33688  erler  33705  rlocaddval  33709  rlocmulval  33710  rloccring  33711  rloc1r  33713  ricdomn1  33729  fracfld  33749  nsgqusf1olem1  33842  nsgqusf1olem2  33843  nsgqusf1olem3  33844  lmhmqusker  33846  rhmquskerlem  33853  elrspunidl  33856  elrspunsn  33857  idlinsubrg  33859  rhmimaidl  33860  mxidlprm  33873  mxidlirredi  33874  mxidlirred  33875  drngmxidlr  33880  opprqusplusg  33891  opprqusmulr  33893  qsdrngi  33897  qsdrng  33899  drnglring  33902  dflring2  33903  dflringlem2  33905  dflringlem3  33906  dflring3  33907  dflring4  33908  rsprprmprmidlb  33933  rprmirred  33941  rprmirredb  33942  rprmdvdsprod  33944  1arithidom  33947  pidufd  33953  1arithufdlem2  33955  1arithufdlem3  33956  1arithufdlem4  33957  dfufd2lem  33959  deg1prod  33993  mplidomlem  34037  mplmulmvr  34049  mplvrpmrhm  34057  psrgsum  34058  psrmonprod  34062  esplyfv  34080  esplyfval1  34083  esplyind  34085  dimkerim  34137  fedgmul  34141  extdg1id  34176  evls1fldgencl  34180  fldextrspunlsplem  34183  fldextrspunlsp  34184  extdgfialglem1  34202  extdgfialg  34204  minplyirred  34221  constrextdg2lem  34258  constrfiss  34261  cos9thpiminplylem2  34293  qtophaus  34346  zarclsint  34382  zarcmplem  34391  esumcst  34573  sigapildsys  34673  oms0  34808  omssubadd  34811  carsgclctunlem3  34831  eulerpartlemgvv  34887  signsply0  35059  signstfvneq0  35080  actfunsnf1o  35112  reprsuc  35123  reprinfz1  35130  breprexplema  35138  breprexplemc  35140  hgt750lemb  35164  cvmlift3lem2  35899  satfdmlem  35947  nn0prpwlem  36941  mblfinlem3  38408  mblfinlem4  38409  itg2addnclem2  38421  itg2gt0cn  38424  ftc1cnnc  38441  ftc1anc  38450  sstotbnd2  38524  lcfl8  42375  aks4d1p8  42953  fldhmf1  42956  mndmolinv  42961  primrootsunit1  42963  primrootscoprmpow  42965  primrootspoweq0  42972  aks6d1c2p2  42985  aks6d1c2lem4  42993  aks6d1c6lem3  43038  aks6d1c7  43050  unitscyglem2  43062  aks5  43070  fiabv  43418  fsuppind  43436  prjspersym  43453  pell1234qrdich  43702  pell14qrdich  43710  pell1qrgap  43715  pellfundex  43727  omabs2  44173  cvgdvgrat  45137  infleinflem2  46200  xrralrecnnle  46212  climrec  46433  climsuse  46438  limcrecl  46459  limsupubuz  46541  limsupgtlem  46605  xlimliminflimsup  46690  fperdvper  46747  dvnprodlem2  46775  etransclem35  47097  hspmbllem2  47455  smflimlem2  47600  smflimlem4  47602  iccpartgt  48327  prproropf1olem4  48406  sfprmdvdsmersenne  48506  gricushgr  48833  2zlidl  49155  ply1mulgsumlem2  49317  nn0sumshdiglemA  49549  imaf1co  50081  uppropd  50107  fuco21  50262  functhinclem4  50373  2arwcat  50526