Theorem ad4antr 733

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 731	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  735  ad5antlr  736  simp-4l  783  tfrlem1  8315  prdsval  17418  catass  17652  catpropd  17675  cidpropd  17676  subccocl  17812  funcco  17838  natpropd  17946  fucpropd  17947  initoeu2lem1  17981  prfval  18165  xpcpropd  18174  acsfiindd  18519  chnind  18587  chnso  18590  mndpsuppss  18733  mhmmnd  19040  ghmqusnsg  19257  ghmquskerlem3  19261  ghmqusker  19262  omndmul2  20108  rhmpreimaidl  21275  rhmqusnsg  21283  mhpmulcl  22115  psdmul  22132  scmatscm  22478  cpmatmcllem  22683  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  chpdmatlem2  22804  chfacfisf  22819  chfacfisfcpmat  22820  neitr  23145  hauscmplem  23371  trcfilu  24258  cfilucfil  24524  restmetu  24535  metucn  24536  cnheibor  24922  dvlip2  25962  lgamucov  27001  bdayfinbndlem1  28459  tgifscgr  28576  iscgrglt  28582  tgbtwnconn1  28643  legtrd  28657  legtri3  28658  legso  28667  hlcgrex  28684  tglndim0  28697  tglinethru  28704  tglnpt2  28709  colline  28717  perpneq  28782  isperp2  28783  footexALT  28786  opphllem  28803  midex  28805  opphllem3  28817  opphllem5  28819  opphllem6  28820  opphl  28822  outpasch  28823  hlpasch  28824  lnopp2hpgb  28831  hpgerlem  28833  lmieu  28852  lnperpex  28871  trgcopy  28872  cgrahl  28895  acopy  28901  inaghl  28913  cgrg3col4  28921  f1otrg  28939  nbumgrvtx  29415  3cyclfrgr  30358  numclwlk2lem2f1o  30449  s3f1  33007  ccatws1f1o  33011  dfmgc2  33056  pwrssmgc  33060  mgcf1o  33063  mndlrinvb  33085  gsumwun  33137  psgnfzto1stlem  33161  cycpmrn  33204  tocyccntz  33205  cycpmconjs  33217  isarchi3  33248  archirngz  33250  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  erler  33326  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rloc1r  33333  fracfld  33369  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  lmhmqusker  33477  rhmquskerlem  33485  elrspunidl  33488  elrspunsn  33489  idlinsubrg  33491  rhmimaidl  33492  drngidl  33493  isprmidlc  33507  qsidomlem1  33512  qsidomlem2  33513  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  mxidlirred  33532  drngmxidlr  33538  opprqusplusg  33549  opprqusmulr  33551  qsdrngi  33555  qsdrng  33557  rsprprmprmidlb  33583  rprmirred  33591  rprmirredb  33592  rprmdvdsprod  33594  1arithidom  33597  pidufd  33603  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  deg1prod  33643  mplmulmvr  33683  mplvrpmrhm  33691  psrgsum  33692  psrmonprod  33696  esplyfv  33714  esplyfval1  33717  esplyind  33719  dimkerim  33771  fedgmul  33775  extdg1id  33810  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem1  33836  extdgfialg  33838  minplyirred  33855  constrextdg2lem  33892  constrfiss  33895  cos9thpiminplylem2  33927  qtophaus  33980  zarclsint  34016  zarcmplem  34025  esumcst  34207  sigapildsys  34306  oms0  34441  omssubadd  34444  carsgclctunlem3  34464  eulerpartlemgvv  34520  signsply0  34695  signstfvneq0  34716  actfunsnf1o  34748  reprsuc  34759  reprinfz1  34766  breprexplema  34774  breprexplemc  34776  hgt750lemb  34800  cvmlift3lem2  35502  satfdmlem  35550  nn0prpwlem  36504  lindsenlbs  37936  matunitlindflem1  37937  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem2  37993  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anc  38022  sstotbnd2  38095  lcfl8  41948  aks4d1p8  42526  fldhmf1  42529  mndmolinv  42534  primrootsunit1  42536  primrootscoprmpow  42538  primrootspoweq0  42545  aks6d1c2p2  42558  aks6d1c2lem4  42566  aks6d1c6lem3  42611  aks6d1c7  42623  unitscyglem2  42635  aks5  42643  fiabv  42981  fsuppind  43023  prjspersym  43040  pell1234qrdich  43289  pell14qrdich  43297  pell1qrgap  43302  pellfundex  43314  omabs2  43760  cvgdvgrat  44740  infleinflem2  45800  xrralrecnnle  45812  climrec  46033  climsuse  46038  limcrecl  46059  limsupubuz  46141  limsupgtlem  46205  xlimliminflimsup  46290  fperdvper  46347  dvnprodlem2  46375  etransclem35  46697  hspmbllem2  47055  smflimlem2  47200  smflimlem4  47202  iccpartgt  47887  prproropf1olem4  47966  sfprmdvdsmersenne  48066  gricushgr  48393  2zlidl  48716  ply1mulgsumlem2  48863  nn0sumshdiglemA  49095  imaf1co  49630  uppropd  49656  fuco21  49811  functhinclem4  49922  2arwcat  50075