Theorem ad4ant13 763

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 485	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 731	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:  ad5ant14  769  ad5ant24  772  ad5ant124  1388  fntpb  7207  peano5  7886  f1o2ndf1  8113  cantnfle  9636  cantnflem1c  9652  ttukeylem5  10492  rlimsqzlem  15696  dvdslcmf  16684  poslubmo  18460  posglbmo  18461  smndex1mgm  18964  isgrpinv  19055  ghmgrp  19127  dprdfcntz  20082  pzriprnglem4  21634  sraassab  22018  cply1coe0bi  22462  evls1fpws  22529  isnrm3  23516  cnextcn  24224  ustexsym  24373  ustex2sym  24374  ustex3sym  24375  trust  24386  fmucnd  24448  trcfilu  24450  metust  24715  cxpmul2z  26856  umgrres1lem  29660  upgrres1  29663  friendshipgt3  30749  ccatf1  33269  cyc3evpm  33470  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem4  33565  elrgspnsubrunlem1  33567  elrgspnsubrunlem2  33568  znfermltl  33681  rhmimaidl  33740  selvply1rhmlema  33908  evlextv  33932  dimlssid  34022  txomap  34224  zart0  34269  repr0  34998  breprexplemc  35019  hgt750lemb  35043  satffunlem1lem2  35895  satffunlem2lem2  35898  lindsadd  38264  matunitlindflem1  38267  nadd1suc  44119  mapss2  45922  supxrge  46054  xrlexaddrp  46068  infxr  46082  infleinf  46087  unb2ltle  46129  supminfxr  46178  limsuppnfdlem  46415  limsupub  46418  limsuppnflem  46424  climinf3  46430  limsupmnflem  46434  climxrre  46464  liminfvalxr  46497  fperdvper  46633  sge0isum  47141  sge0gtfsumgt  47157  sge0seq  47160  nnfoctbdjlem  47169  meaiuninc3v  47198  omeiunltfirp  47233  hspdifhsp  47330  hspmbllem2  47341  pimdecfgtioo  47431  pimincfltioo  47432  preimageiingt  47434  preimaleiinlt  47435  smfid  47466  proththd  48366