Theorem ad4antr 738

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad5antr  740  ad5antlr  741  simp-4l  788  tfrlem1  8312  prdsval  17416  catass  17650  catpropd  17673  cidpropd  17674  subccocl  17810  funcco  17836  natpropd  17944  fucpropd  17945  initoeu2lem1  17979  prfval  18163  xpcpropd  18172  acsfiindd  18517  chnind  18585  chnso  18588  mndpsuppss  18731  mhmmnd  19038  ghmqusnsg  19255  ghmquskerlem3  19259  ghmqusker  19260  omndmul2  20106  rhmpreimaidl  21277  rhmqusnsg  21285  mhpmulcl  22144  psdmul  22161  scmatscm  22503  cpmatmcllem  22708  mptcoe1matfsupp  22792  mp2pm2mplem4  22799  chpdmatlem2  22829  chfacfisf  22844  chfacfisfcpmat  22845  neitr  23170  hauscmplem  23396  trcfilu  24283  cfilucfil  24549  restmetu  24560  metucn  24561  cnheibor  24947  dvlip2  25987  lgamucov  27026  bdayfinbndlem1  28484  tgifscgr  28601  iscgrglt  28607  tgbtwnconn1  28668  legtrd  28682  legtri3  28683  legso  28692  hlcgrex  28709  tglndim0  28722  tglinethru  28729  tglnpt2  28734  colline  28742  perpneq  28807  isperp2  28808  footexALT  28811  opphllem  28828  midex  28830  opphllem3  28842  opphllem5  28844  opphllem6  28845  opphl  28847  outpasch  28848  hlpasch  28849  lnopp2hpgb  28856  hpgerlem  28858  lmieu  28877  lnperpex  28896  trgcopy  28897  cgrahl  28920  acopy  28926  inaghl  28938  cgrg3col4  28946  f1otrg  28964  nbumgrvtx  29440  3cyclfrgr  30383  numclwlk2lem2f1o  30474  s3f1  33033  ccatws1f1o  33037  dfmgc2  33082  pwrssmgc  33086  mgcf1o  33089  mndlrinvb  33111  gsumwun  33164  psgnfzto1stlem  33188  cycpmrn  33231  tocyccntz  33232  cycpmconjs  33244  isarchi3  33275  archirngz  33277  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem2  33336  erler  33353  rlocaddval  33356  rlocmulval  33357  rloccring  33358  rloc1r  33360  ricdomn1  33377  fracfld  33399  nsgqusf1olem1  33503  nsgqusf1olem2  33504  nsgqusf1olem3  33505  lmhmqusker  33507  rhmquskerlem  33515  elrspunidl  33518  elrspunsn  33519  idlinsubrg  33521  rhmimaidl  33522  drngidl  33523  isprmidlc  33537  qsidomlem1  33542  qsidomlem2  33543  ssdifidlprm  33548  mxidlprm  33560  mxidlirredi  33561  mxidlirred  33562  drngmxidlr  33568  opprqusplusg  33579  opprqusmulr  33581  qsdrngi  33585  qsdrng  33587  rsprprmprmidlb  33613  rprmirred  33621  rprmirredb  33622  rprmdvdsprod  33624  1arithidom  33627  pidufd  33633  1arithufdlem2  33635  1arithufdlem3  33636  1arithufdlem4  33637  dfufd2lem  33639  deg1prod  33673  mplidomlem  33718  mplmulmvr  33730  mplvrpmrhm  33738  psrgsum  33739  psrmonprod  33743  esplyfv  33761  esplyfval1  33764  esplyind  33766  dimkerim  33818  fedgmul  33822  extdg1id  33857  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  extdgfialglem1  33883  extdgfialg  33885  minplyirred  33902  constrextdg2lem  33939  constrfiss  33942  cos9thpiminplylem2  33974  qtophaus  34027  zarclsint  34063  zarcmplem  34072  esumcst  34254  sigapildsys  34353  oms0  34488  omssubadd  34491  carsgclctunlem3  34511  eulerpartlemgvv  34567  signsply0  34742  signstfvneq0  34763  actfunsnf1o  34795  reprsuc  34806  reprinfz1  34813  breprexplema  34821  breprexplemc  34823  hgt750lemb  34847  cvmlift3lem2  35555  satfdmlem  35603  nn0prpwlem  36557  lindsenlbs  37989  matunitlindflem1  37990  mblfinlem3  38033  mblfinlem4  38034  itg2addnclem2  38046  itg2gt0cn  38049  ftc1cnnc  38066  ftc1anc  38075  sstotbnd2  38148  lcfl8  42001  aks4d1p8  42579  fldhmf1  42582  mndmolinv  42587  primrootsunit1  42589  primrootscoprmpow  42591  primrootspoweq0  42598  aks6d1c2p2  42611  aks6d1c2lem4  42619  aks6d1c6lem3  42664  aks6d1c7  42676  unitscyglem2  42688  aks5  42696  fiabv  43029  fsuppind  43047  prjspersym  43064  pell1234qrdich  43313  pell14qrdich  43321  pell1qrgap  43326  pellfundex  43338  omabs2  43784  cvgdvgrat  44764  infleinflem2  45822  xrralrecnnle  45834  climrec  46055  climsuse  46060  limcrecl  46081  limsupubuz  46163  limsupgtlem  46227  xlimliminflimsup  46312  fperdvper  46369  dvnprodlem2  46397  etransclem35  46719  hspmbllem2  47077  smflimlem2  47222  smflimlem4  47224  iccpartgt  47909  prproropf1olem4  47988  sfprmdvdsmersenne  48088  gricushgr  48415  2zlidl  48738  ply1mulgsumlem2  48885  nn0sumshdiglemA  49117  imaf1co  49652  uppropd  49678  fuco21  49833  functhinclem4  49944  2arwcat  50097