Theorem ad4antr 742

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad5antr  744  ad5antlr  745  simp-4l  792  tfrlem1  8339  prdsval  17474  catass  17708  catpropd  17731  cidpropd  17732  subccocl  17868  funcco  17894  natpropd  18002  fucpropd  18003  initoeu2lem1  18037  prfval  18221  xpcpropd  18230  acsfiindd  18575  chnind  18643  chnso  18646  mndpsuppss  18789  mhmmnd  19096  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  omndmul2  20163  rhmpreimaidl  21334  rhmqusnsg  21342  mhpmulcl  22201  psdmul  22218  scmatscm  22560  cpmatmcllem  22765  mptcoe1matfsupp  22849  mp2pm2mplem4  22856  chpdmatlem2  22886  chfacfisf  22901  chfacfisfcpmat  22902  neitr  23227  hauscmplem  23453  trcfilu  24340  cfilucfil  24606  restmetu  24617  metucn  24618  cnheibor  25004  dvlip2  26044  lgamucov  27089  bdayfinbndlem1  28547  tgifscgr  28664  iscgrglt  28670  tgbtwnconn1  28731  legtrd  28745  legtri3  28746  legso  28755  hlcgrex  28772  tglndim0  28785  tglinethru  28792  tglnpt2  28797  colline  28805  perpneq  28870  isperp2  28871  footexALT  28874  opphllem  28891  midex  28893  opphllem3  28905  opphllem5  28907  opphllem6  28908  opphl  28910  outpasch  28911  hlpasch  28912  lnopp2hpgb  28919  hpgerlem  28921  lmieu  28940  lnperpex  28959  trgcopy  28960  cgrahl  28983  acopy  28989  inaghl  29001  cgrg3col4  29009  f1otrg  29027  nbumgrvtx  29503  3cyclfrgr  30446  numclwlk2lem2f1o  30537  s3f1  33085  ccatws1f1o  33089  dfmgc2  33134  pwrssmgc  33138  mgcf1o  33141  mndlrinvb  33163  gsumwun  33216  psgnfzto1stlem  33240  cycpmrn  33283  tocyccntz  33284  cycpmconjs  33296  isarchi3  33327  archirngz  33329  elrgspnlem2  33384  elrgspnlem4  33386  elrgspnsubrunlem2  33389  erler  33406  rlocaddval  33410  rlocmulval  33411  rloccring  33412  rloc1r  33414  ricdomn1  33433  fracfld  33455  nsgqusf1olem1  33559  nsgqusf1olem2  33560  nsgqusf1olem3  33561  lmhmqusker  33563  rhmquskerlem  33571  elrspunidl  33574  elrspunsn  33575  idlinsubrg  33577  rhmimaidl  33578  drngidl  33579  isprmidlc  33593  qsidomlem1  33599  qsidomlem2  33600  ssdifidlprm  33605  mxidlprm  33618  mxidlirredi  33619  mxidlirred  33620  drngmxidlr  33626  opprqusplusg  33637  opprqusmulr  33639  qsdrngi  33643  qsdrng  33645  drnglring  33648  dflring2  33649  dflringlem2  33651  dflringlem3  33652  dflring3  33653  dflring4  33654  rsprprmprmidlb  33679  rprmirred  33687  rprmirredb  33688  rprmdvdsprod  33690  1arithidom  33693  pidufd  33699  1arithufdlem2  33701  1arithufdlem3  33702  1arithufdlem4  33703  dfufd2lem  33705  deg1prod  33739  mplidomlem  33784  mplmulmvr  33796  mplvrpmrhm  33804  psrgsum  33805  psrmonprod  33809  esplyfv  33827  esplyfval1  33830  esplyind  33832  dimkerim  33884  fedgmul  33888  extdg1id  33923  evls1fldgencl  33927  fldextrspunlsplem  33930  fldextrspunlsp  33931  extdgfialglem1  33949  extdgfialg  33951  minplyirred  33968  constrextdg2lem  34005  constrfiss  34008  cos9thpiminplylem2  34040  qtophaus  34093  zarclsint  34129  zarcmplem  34138  esumcst  34320  sigapildsys  34419  oms0  34554  omssubadd  34557  carsgclctunlem3  34577  eulerpartlemgvv  34633  signsply0  34805  signstfvneq0  34826  actfunsnf1o  34858  reprsuc  34869  reprinfz1  34876  breprexplema  34884  breprexplemc  34886  hgt750lemb  34910  cvmlift3lem2  35630  satfdmlem  35678  nn0prpwlem  36642  lindsenlbs  38074  matunitlindflem1  38075  mblfinlem3  38118  mblfinlem4  38119  itg2addnclem2  38131  itg2gt0cn  38134  ftc1cnnc  38151  ftc1anc  38160  sstotbnd2  38233  lcfl8  42086  aks4d1p8  42664  fldhmf1  42667  mndmolinv  42672  primrootsunit1  42674  primrootscoprmpow  42676  primrootspoweq0  42683  aks6d1c2p2  42696  aks6d1c2lem4  42704  aks6d1c6lem3  42749  aks6d1c7  42761  unitscyglem2  42773  aks5  42781  fiabv  43114  fsuppind  43132  prjspersym  43149  pell1234qrdich  43398  pell14qrdich  43406  pell1qrgap  43411  pellfundex  43423  omabs2  43869  cvgdvgrat  44849  infleinflem2  45906  xrralrecnnle  45918  climrec  46139  climsuse  46144  limcrecl  46165  limsupubuz  46247  limsupgtlem  46311  xlimliminflimsup  46396  fperdvper  46453  dvnprodlem2  46481  etransclem35  46803  hspmbllem2  47161  smflimlem2  47306  smflimlem4  47308  iccpartgt  47993  prproropf1olem4  48072  sfprmdvdsmersenne  48172  gricushgr  48499  2zlidl  48822  ply1mulgsumlem2  48969  nn0sumshdiglemA  49201  imaf1co  49736  uppropd  49762  fuco21  49917  functhinclem4  50028  2arwcat  50181