Theorem ad4antr 732

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5antr  734  ad5antlr  735  simp-4l  782  tfrlem1  8347  prdsval  17425  catass  17654  catpropd  17677  cidpropd  17678  subccocl  17814  funcco  17840  natpropd  17948  fucpropd  17949  initoeu2lem1  17983  prfval  18167  xpcpropd  18176  acsfiindd  18519  mndpsuppss  18699  mhmmnd  19003  ghmqusnsg  19221  ghmquskerlem3  19225  ghmqusker  19226  rhmpreimaidl  21194  rhmqusnsg  21202  mhpmulcl  22043  psdmul  22060  scmatscm  22407  cpmatmcllem  22612  mptcoe1matfsupp  22696  mp2pm2mplem4  22703  chpdmatlem2  22733  chfacfisf  22748  chfacfisfcpmat  22749  neitr  23074  hauscmplem  23300  trcfilu  24188  cfilucfil  24454  restmetu  24465  metucn  24466  cnheibor  24861  dvlip2  25907  lgamucov  26955  tgifscgr  28442  iscgrglt  28448  tgbtwnconn1  28509  legtrd  28523  legtri3  28524  legso  28533  hlcgrex  28550  tglndim0  28563  tglinethru  28570  tglnpt2  28575  colline  28583  perpneq  28648  isperp2  28649  footexALT  28652  opphllem  28669  midex  28671  opphllem3  28683  opphllem5  28685  opphllem6  28686  opphl  28688  outpasch  28689  hlpasch  28690  lnopp2hpgb  28697  hpgerlem  28699  lmieu  28718  lnperpex  28737  trgcopy  28738  cgrahl  28761  acopy  28767  inaghl  28779  cgrg3col4  28787  f1otrg  28805  nbumgrvtx  29280  3cyclfrgr  30224  numclwlk2lem2f1o  30315  s3f1  32875  ccatws1f1o  32880  dfmgc2  32929  pwrssmgc  32933  mgcf1o  32936  chnind  32944  chnso  32947  mndlrinvb  32973  gsumwun  33012  omndmul2  33033  psgnfzto1stlem  33064  cycpmrn  33107  tocyccntz  33108  cycpmconjs  33120  isarchi3  33148  archirngz  33150  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  erler  33223  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rloc1r  33230  fracfld  33265  nsgqusf1olem1  33391  nsgqusf1olem2  33392  nsgqusf1olem3  33393  lmhmqusker  33395  rhmquskerlem  33403  elrspunidl  33406  elrspunsn  33407  idlinsubrg  33409  rhmimaidl  33410  drngidl  33411  isprmidlc  33425  qsidomlem1  33430  qsidomlem2  33431  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  mxidlirred  33450  drngmxidlr  33456  opprqusplusg  33467  opprqusmulr  33469  qsdrngi  33473  qsdrng  33475  rsprprmprmidlb  33501  rprmirred  33509  rprmirredb  33510  rprmdvdsprod  33512  1arithidom  33515  pidufd  33521  1arithufdlem2  33523  1arithufdlem3  33524  1arithufdlem4  33525  dfufd2lem  33527  dimkerim  33630  fedgmul  33634  extdg1id  33668  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  minplyirred  33708  constrextdg2lem  33745  constrfiss  33748  cos9thpiminplylem2  33780  qtophaus  33833  zarclsint  33869  zarcmplem  33878  esumcst  34060  sigapildsys  34159  oms0  34295  omssubadd  34298  carsgclctunlem3  34318  eulerpartlemgvv  34374  signsply0  34549  signstfvneq0  34570  actfunsnf1o  34602  reprsuc  34613  reprinfz1  34620  breprexplema  34628  breprexplemc  34630  hgt750lemb  34654  cvmlift3lem2  35314  satfdmlem  35362  nn0prpwlem  36317  lindsenlbs  37616  matunitlindflem1  37617  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem2  37673  itg2gt0cn  37676  ftc1cnnc  37693  ftc1anc  37702  sstotbnd2  37775  lcfl8  41503  aks4d1p8  42082  fldhmf1  42085  mndmolinv  42090  primrootsunit1  42092  primrootscoprmpow  42094  primrootspoweq0  42101  aks6d1c2p2  42114  aks6d1c2lem4  42122  aks6d1c6lem3  42167  aks6d1c7  42179  unitscyglem2  42191  aks5  42199  fiabv  42531  fsuppind  42585  prjspersym  42602  pell1234qrdich  42856  pell14qrdich  42864  pell1qrgap  42869  pellfundex  42881  omabs2  43328  cvgdvgrat  44309  infleinflem2  45374  xrralrecnnle  45386  climrec  45608  climsuse  45613  limcrecl  45634  limsupubuz  45718  limsupgtlem  45782  xlimliminflimsup  45867  fperdvper  45924  dvnprodlem2  45952  etransclem35  46274  hspmbllem2  46632  smflimlem2  46777  smflimlem4  46779  iccpartgt  47432  prproropf1olem4  47511  sfprmdvdsmersenne  47608  gricushgr  47921  2zlidl  48232  ply1mulgsumlem2  48380  nn0sumshdiglemA  48612  imaf1co  49148  uppropd  49174  fuco21  49329  functhinclem4  49440  2arwcat  49593