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  7219  peano5  7909  f1o2ndf1  8139  cantnfle  9679  cantnflem1c  9695  ttukeylem5  10598  ccatf1  14743  rlimsqzlem  15825  dvdslcmf  16815  poslubmo  18592  posglbmo  18593  smndex1mgm  19115  isgrpinv  19213  ghmgrp  19285  dprdfcntz  20240  pzriprnglem4  21799  sraassab  22185  cply1coe0bi  22629  evls1fpws  22696  matunitlindflem1  23003  isnrm3  23686  cnextcn  24395  ustexsym  24544  ustex2sym  24545  ustex3sym  24546  trust  24557  fmucnd  24619  trcfilu  24621  metust  24886  cxpmul2z  27028  umgrres1lem  29900  upgrres1  29903  friendshipgt3  31008  cyc3evpm  33761  elrgspnlem1  33853  elrgspnlem2  33854  elrgspnlem4  33856  elrgspnsubrunlem1  33858  elrgspnsubrunlem2  33859  znfermltl  33972  rhmimaidl  34032  selvply1rhmlema  34200  evlextv  34224  dimlssid  34314  txomap  34516  reff  34521  zart0  34561  repr0  35290  breprexplemc  35311  hgt750lemb  35335  satffunlem1lem2  36258  satffunlem2lem2  36261  lindsadd  38645  nadd1suc  44503  mapss2  46327  supxrge  46458  xrlexaddrp  46472  infxr  46486  infleinf  46491  unb2ltle  46533  supminfxr  46582  limsuppnfdlem  46819  limsupub  46822  limsuppnflem  46828  climinf3  46834  limsupmnflem  46838  climxrre  46868  liminfvalxr  46901  fperdvper  47037  sge0isum  47545  sge0gtfsumgt  47561  sge0seq  47564  nnfoctbdjlem  47573  meaiuninc3v  47602  omeiunltfirp  47637  hspdifhsp  47734  hspmbllem2  47745  pimdecfgtioo  47835  pimincfltioo  47836  preimageiingt  47838  preimaleiinlt  47839  smfid  47870  proththd  48807