Theorem ad4ant13 764

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 486	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 732	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant14  770  ad5ant24  773  ad5ant124  1388  fntpb  7208  peano5  7890  f1o2ndf1  8119  cantnfle  9650  cantnflem1c  9666  ttukeylem5  10515  ccatf1  14656  rlimsqzlem  15736  dvdslcmf  16721  poslubmo  18497  posglbmo  18498  smndex1mgm  19019  isgrpinv  19117  ghmgrp  19189  dprdfcntz  20144  pzriprnglem4  21697  sraassab  22083  cply1coe0bi  22527  evls1fpws  22594  matunitlindflem1  22901  isnrm3  23584  cnextcn  24293  ustexsym  24442  ustex2sym  24443  ustex3sym  24444  trust  24455  fmucnd  24517  trcfilu  24519  metust  24784  cxpmul2z  26928  umgrres1lem  29770  upgrres1  29773  friendshipgt3  30878  cyc3evpm  33590  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem4  33685  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  znfermltl  33801  rhmimaidl  33860  selvply1rhmlema  34028  evlextv  34052  dimlssid  34142  txomap  34344  zart0  34389  repr0  35119  breprexplemc  35140  hgt750lemb  35164  satffunlem1lem2  35982  satffunlem2lem2  35985  lindsadd  38367  nadd1suc  44233  mapss2  46036  supxrge  46168  xrlexaddrp  46182  infxr  46196  infleinf  46201  unb2ltle  46243  supminfxr  46292  limsuppnfdlem  46529  limsupub  46532  limsuppnflem  46538  climinf3  46544  limsupmnflem  46548  climxrre  46578  liminfvalxr  46611  fperdvper  46747  sge0isum  47255  sge0gtfsumgt  47271  sge0seq  47274  nnfoctbdjlem  47283  meaiuninc3v  47312  omeiunltfirp  47347  hspdifhsp  47444  hspmbllem2  47455  pimdecfgtioo  47545  pimincfltioo  47546  preimageiingt  47548  preimaleiinlt  47549  smfid  47580  proththd  48517