Theorem ad4ant13 761

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant13	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 484	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 729	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad5ant14  767  ad5ant24  770  ad5ant124  1380  fntpb  7193  peano5  7874  f1o2ndf1  8101  cantnfle  9626  cantnflem1c  9642  ttukeylem5  10470  rlimsqzlem  15676  dvdslcmf  16665  poslubmo  18441  posglbmo  18442  smndex1mgm  18944  isgrpinv  19035  ghmgrp  19108  dprdfcntz  20057  pzriprnglem4  21533  sraassab  21917  cply1coe0bi  22362  evls1fpws  22429  isnrm3  23416  cnextcn  24124  ustexsym  24273  ustex2sym  24274  ustex3sym  24275  trust  24286  fmucnd  24348  trcfilu  24350  metust  24615  cxpmul2z  26753  umgrres1lem  29508  upgrres1  29511  friendshipgt3  30597  ccatf1  33124  cyc3evpm  33327  elrgspnlem1  33420  elrgspnlem2  33421  elrgspnlem4  33423  elrgspnsubrunlem1  33425  elrgspnsubrunlem2  33426  znfermltl  33549  rhmimaidl  33615  selvply1rhmlema  33812  evlextv  33836  dimlssid  33926  txomap  34128  zart0  34173  repr0  34902  breprexplemc  34923  hgt750lemb  34947  satffunlem1lem2  35750  satffunlem2lem2  35753  lindsadd  38109  matunitlindflem1  38112  nadd1suc  43966  mapss2  45779  supxrge  45911  xrlexaddrp  45925  infxr  45939  infleinf  45944  unb2ltle  45986  supminfxr  46035  limsuppnfdlem  46272  limsupub  46275  limsuppnflem  46281  climinf3  46287  limsupmnflem  46291  climxrre  46321  liminfvalxr  46354  fperdvper  46490  sge0isum  46998  sge0gtfsumgt  47014  sge0seq  47017  nnfoctbdjlem  47026  meaiuninc3v  47055  omeiunltfirp  47090  hspdifhsp  47187  hspmbllem2  47198  pimdecfgtioo  47288  pimincfltioo  47289  preimageiingt  47291  preimaleiinlt  47292  smfid  47323  proththd  48220