Theorem ad4ant13 752

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 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 720	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:  ad5ant14  758  ad5ant24  761  fntpb  7158  peano5  7838  f1o2ndf1  8066  cantnfle  9586  cantnflem1c  9602  ttukeylem5  10429  rlimsqzlem  15605  dvdslcmf  16594  poslubmo  18369  posglbmo  18370  smndex1mgm  18872  isgrpinv  18963  ghmgrp  19036  dprdfcntz  19986  pzriprnglem4  21477  sraassab  21861  cply1coe0bi  22280  evls1fpws  22347  isnrm3  23337  cnextcn  24045  ustexsym  24194  ustex2sym  24195  ustex3sym  24196  trust  24207  fmucnd  24269  trcfilu  24271  metust  24536  cxpmul2z  26671  umgrres1lem  29396  upgrres1  29399  friendshipgt3  30486  ccatf1  33027  cyc3evpm  33229  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem4  33324  elrgspnsubrunlem1  33326  elrgspnsubrunlem2  33327  znfermltl  33444  rhmimaidl  33510  evlextv  33704  dimlssid  33795  txomap  33997  zart0  34042  repr0  34774  breprexplemc  34795  hgt750lemb  34819  satffunlem1lem2  35604  satffunlem2lem2  35607  lindsadd  37951  matunitlindflem1  37954  nadd1suc  43841  mapss2  45655  supxrge  45789  xrlexaddrp  45803  infxr  45817  infleinf  45822  unb2ltle  45864  supminfxr  45913  limsuppnfdlem  46150  limsupub  46153  limsuppnflem  46159  climinf3  46165  limsupmnflem  46169  climxrre  46199  liminfvalxr  46232  fperdvper  46368  sge0isum  46876  sge0gtfsumgt  46892  sge0seq  46895  nnfoctbdjlem  46904  meaiuninc3v  46933  omeiunltfirp  46968  hspdifhsp  47065  hspmbllem2  47076  pimdecfgtioo  47166  pimincfltioo  47167  preimageiingt  47169  preimaleiinlt  47170  smfid  47201  proththd  48092