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  8307  prdsval  17375  catass  17609  catpropd  17632  cidpropd  17633  subccocl  17769  funcco  17795  natpropd  17903  fucpropd  17904  initoeu2lem1  17938  prfval  18122  xpcpropd  18131  acsfiindd  18476  chnind  18544  chnso  18547  mndpsuppss  18690  mhmmnd  18994  ghmqusnsg  19211  ghmquskerlem3  19215  ghmqusker  19216  omndmul2  20062  rhmpreimaidl  21232  rhmqusnsg  21240  mhpmulcl  22092  psdmul  22109  scmatscm  22457  cpmatmcllem  22662  mptcoe1matfsupp  22746  mp2pm2mplem4  22753  chpdmatlem2  22783  chfacfisf  22798  chfacfisfcpmat  22799  neitr  23124  hauscmplem  23350  trcfilu  24237  cfilucfil  24503  restmetu  24514  metucn  24515  cnheibor  24910  dvlip2  25956  lgamucov  27004  bdayfinbndlem1  28463  tgifscgr  28580  iscgrglt  28586  tgbtwnconn1  28647  legtrd  28661  legtri3  28662  legso  28671  hlcgrex  28688  tglndim0  28701  tglinethru  28708  tglnpt2  28713  colline  28721  perpneq  28786  isperp2  28787  footexALT  28790  opphllem  28807  midex  28809  opphllem3  28821  opphllem5  28823  opphllem6  28824  opphl  28826  outpasch  28827  hlpasch  28828  lnopp2hpgb  28835  hpgerlem  28837  lmieu  28856  lnperpex  28875  trgcopy  28876  cgrahl  28899  acopy  28905  inaghl  28917  cgrg3col4  28925  f1otrg  28943  nbumgrvtx  29419  3cyclfrgr  30363  numclwlk2lem2f1o  30454  s3f1  33029  ccatws1f1o  33033  dfmgc2  33078  pwrssmgc  33082  mgcf1o  33085  mndlrinvb  33107  gsumwun  33158  psgnfzto1stlem  33182  cycpmrn  33225  tocyccntz  33226  cycpmconjs  33238  isarchi3  33269  archirngz  33271  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem2  33330  erler  33347  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rloc1r  33354  fracfld  33390  nsgqusf1olem1  33494  nsgqusf1olem2  33495  nsgqusf1olem3  33496  lmhmqusker  33498  rhmquskerlem  33506  elrspunidl  33509  elrspunsn  33510  idlinsubrg  33512  rhmimaidl  33513  drngidl  33514  isprmidlc  33528  qsidomlem1  33533  qsidomlem2  33534  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  mxidlirred  33553  drngmxidlr  33559  opprqusplusg  33570  opprqusmulr  33572  qsdrngi  33576  qsdrng  33578  rsprprmprmidlb  33604  rprmirred  33612  rprmirredb  33613  rprmdvdsprod  33615  1arithidom  33618  pidufd  33624  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  deg1prod  33664  mplmulmvr  33704  mplvrpmrhm  33712  esplyfv  33728  esplyind  33731  dimkerim  33784  fedgmul  33788  extdg1id  33823  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem1  33849  extdgfialg  33851  minplyirred  33868  constrextdg2lem  33905  constrfiss  33908  cos9thpiminplylem2  33940  qtophaus  33993  zarclsint  34029  zarcmplem  34038  esumcst  34220  sigapildsys  34319  oms0  34454  omssubadd  34457  carsgclctunlem3  34477  eulerpartlemgvv  34533  signsply0  34708  signstfvneq0  34729  actfunsnf1o  34761  reprsuc  34772  reprinfz1  34779  breprexplema  34787  breprexplemc  34789  hgt750lemb  34813  cvmlift3lem2  35514  satfdmlem  35562  nn0prpwlem  36516  lindsenlbs  37816  matunitlindflem1  37817  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem2  37873  itg2gt0cn  37876  ftc1cnnc  37893  ftc1anc  37902  sstotbnd2  37975  lcfl8  41762  aks4d1p8  42341  fldhmf1  42344  mndmolinv  42349  primrootsunit1  42351  primrootscoprmpow  42353  primrootspoweq0  42360  aks6d1c2p2  42373  aks6d1c2lem4  42381  aks6d1c6lem3  42426  aks6d1c7  42438  unitscyglem2  42450  aks5  42458  fiabv  42791  fsuppind  42833  prjspersym  42850  pell1234qrdich  43103  pell14qrdich  43111  pell1qrgap  43116  pellfundex  43128  omabs2  43574  cvgdvgrat  44554  infleinflem2  45615  xrralrecnnle  45627  climrec  45849  climsuse  45854  limcrecl  45875  limsupubuz  45957  limsupgtlem  46021  xlimliminflimsup  46106  fperdvper  46163  dvnprodlem2  46191  etransclem35  46513  hspmbllem2  46871  smflimlem2  47016  smflimlem4  47018  iccpartgt  47673  prproropf1olem4  47752  sfprmdvdsmersenne  47849  gricushgr  48163  2zlidl  48486  ply1mulgsumlem2  48633  nn0sumshdiglemA  48865  imaf1co  49400  uppropd  49426  fuco21  49581  functhinclem4  49692  2arwcat  49845