Theorem ad4antr 744

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad5antr  746  ad5antlr  747  simp-4l  794  tfrlem1  8363  prdsval  17509  catass  17743  catpropd  17766  cidpropd  17767  subccocl  17903  funcco  17929  natpropd  18037  fucpropd  18038  initoeu2lem1  18072  prfval  18256  xpcpropd  18265  acsfiindd  18610  chnind  18678  chnso  18681  mndpsuppss  18824  mhmmnd  19131  ghmqusnsg  19353  ghmquskerlem3  19357  ghmqusker  19358  omndmul2  20204  drngidl  21366  rhmpreimaidl  21397  rhmqusnsg  21406  isprmidlc  21453  qsidomlem1  21461  qsidomlem2  21462  ssdifidlprm  21467  mhpmulcl  22293  psdmul  22310  scmatscm  22651  cpmatmcllem  22856  mptcoe1matfsupp  22940  mp2pm2mplem4  22947  chpdmatlem2  22977  chfacfisf  22992  chfacfisfcpmat  22993  neitr  23318  hauscmplem  23544  trcfilu  24431  cfilucfil  24697  restmetu  24708  metucn  24709  cnheibor  25095  dvlip2  26135  lgamucov  27183  bdayfinbndlem1  28641  tgifscgr  28758  iscgrglt  28764  tgbtwnconn1  28825  legtrd  28839  legtri3  28840  legso  28849  hlcgrex  28869  tglndim0  28883  tglinethru  28890  tglinesseq  28894  colline  28904  tglnpt2  28907  tglnpt4  28909  perpneq  28975  isperp2  28976  footexALT  28979  opphllem  28997  midex  28999  opphllem3  29011  opphllem5  29013  opphllem6  29014  opphl  29016  outpasch  29018  hlpasch  29019  lnopp2hpgb  29026  hpgerlem  29028  lnincplng  29047  plngcplem  29048  plngrotlem1  29050  lnssplnglem  29054  lnssplng  29055  plng3p  29060  lmieu  29074  lnperpex  29094  trgcopy  29096  cgrahl  29119  acopy  29125  inaghl  29143  cgrg3col4  29151  prlnghpg  29177  dfprlng2  29178  dfprlng3  29179  perpprlng  29181  prlngex  29182  prlngmolem1  29183  prlngmolem2  29184  quadcgrprlng  29197  f1otrg  29201  nbumgrvtx  29677  3cyclfrgr  30620  numclwlk2lem2f1o  30711  s3f1  33248  ccatws1f1o  33252  dfmgc2  33297  pwrssmgc  33301  mgcf1o  33304  mndlrinvb  33326  gsumwun  33377  psgnfzto1stlem  33401  cycpmrn  33444  tocyccntz  33445  cycpmconjs  33457  isarchi3  33488  archirngz  33490  elrgspnlem2  33544  elrgspnlem4  33546  elrgspnsubrunlem2  33549  erler  33566  rlocaddval  33570  rlocmulval  33571  rloccring  33572  rloc1r  33574  ricdomn1  33590  fracfld  33610  nsgqusf1olem1  33703  nsgqusf1olem2  33704  nsgqusf1olem3  33705  lmhmqusker  33707  rhmquskerlem  33714  elrspunidl  33717  elrspunsn  33718  idlinsubrg  33720  rhmimaidl  33721  mxidlprm  33734  mxidlirredi  33735  mxidlirred  33736  drngmxidlr  33741  opprqusplusg  33752  opprqusmulr  33754  qsdrngi  33758  qsdrng  33760  drnglring  33763  dflring2  33764  dflringlem2  33766  dflringlem3  33767  dflring3  33768  dflring4  33769  rsprprmprmidlb  33794  rprmirred  33802  rprmirredb  33803  rprmdvdsprod  33805  1arithidom  33808  pidufd  33814  1arithufdlem2  33816  1arithufdlem3  33817  1arithufdlem4  33818  dfufd2lem  33820  deg1prod  33854  mplidomlem  33898  mplmulmvr  33910  mplvrpmrhm  33918  psrgsum  33919  psrmonprod  33923  esplyfv  33941  esplyfval1  33944  esplyind  33946  dimkerim  33998  fedgmul  34002  extdg1id  34037  evls1fldgencl  34041  fldextrspunlsplem  34044  fldextrspunlsp  34045  extdgfialglem1  34063  extdgfialg  34065  minplyirred  34082  constrextdg2lem  34119  constrfiss  34122  cos9thpiminplylem2  34154  qtophaus  34207  zarclsint  34243  zarcmplem  34252  esumcst  34434  sigapildsys  34533  oms0  34668  omssubadd  34671  carsgclctunlem3  34691  eulerpartlemgvv  34747  signsply0  34919  signstfvneq0  34940  actfunsnf1o  34972  reprsuc  34983  reprinfz1  34990  breprexplema  34998  breprexplemc  35000  hgt750lemb  35024  cvmlift3lem2  35793  satfdmlem  35841  nn0prpwlem  36814  lindsenlbs  38247  matunitlindflem1  38248  mblfinlem3  38291  mblfinlem4  38292  itg2addnclem2  38304  itg2gt0cn  38307  ftc1cnnc  38324  ftc1anc  38333  sstotbnd2  38406  lcfl8  42257  aks4d1p8  42835  fldhmf1  42838  mndmolinv  42843  primrootsunit1  42845  primrootscoprmpow  42847  primrootspoweq0  42854  aks6d1c2p2  42867  aks6d1c2lem4  42875  aks6d1c6lem3  42920  aks6d1c7  42932  unitscyglem2  42944  aks5  42952  fiabv  43287  fsuppind  43305  prjspersym  43322  pell1234qrdich  43571  pell14qrdich  43579  pell1qrgap  43584  pellfundex  43596  omabs2  44042  cvgdvgrat  45006  infleinflem2  46069  xrralrecnnle  46081  climrec  46302  climsuse  46307  limcrecl  46328  limsupubuz  46410  limsupgtlem  46474  xlimliminflimsup  46559  fperdvper  46616  dvnprodlem2  46644  etransclem35  46966  hspmbllem2  47324  smflimlem2  47469  smflimlem4  47471  iccpartgt  48159  prproropf1olem4  48238  sfprmdvdsmersenne  48338  gricushgr  48665  2zlidl  48988  ply1mulgsumlem2  49150  nn0sumshdiglemA  49382  imaf1co  49916  uppropd  49942  fuco21  50097  functhinclem4  50208  2arwcat  50361