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  7165  peano5  7845  f1o2ndf1  8074  cantnfle  9592  cantnflem1c  9608  ttukeylem5  10435  rlimsqzlem  15584  dvdslcmf  16570  poslubmo  18344  posglbmo  18345  smndex1mgm  18844  isgrpinv  18935  ghmgrp  19008  dprdfcntz  19958  pzriprnglem4  21451  sraassab  21835  cply1coe0bi  22258  evls1fpws  22325  isnrm3  23315  cnextcn  24023  ustexsym  24172  ustex2sym  24173  ustex3sym  24174  trust  24185  fmucnd  24247  trcfilu  24249  metust  24514  cxpmul2z  26668  umgrres1lem  29395  upgrres1  29398  friendshipgt3  30485  ccatf1  33042  cyc3evpm  33244  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem4  33339  elrgspnsubrunlem1  33341  elrgspnsubrunlem2  33342  znfermltl  33459  rhmimaidl  33525  evlextv  33719  dimlssid  33810  txomap  34012  zart0  34057  repr0  34789  breprexplemc  34810  hgt750lemb  34834  satffunlem1lem2  35619  satffunlem2lem2  35622  lindsadd  37864  matunitlindflem1  37867  nadd1suc  43749  mapss2  45563  supxrge  45697  xrlexaddrp  45711  infxr  45725  infleinf  45730  unb2ltle  45773  supminfxr  45822  limsuppnfdlem  46059  limsupub  46062  limsuppnflem  46068  climinf3  46074  limsupmnflem  46078  climxrre  46108  liminfvalxr  46141  fperdvper  46277  sge0isum  46785  sge0gtfsumgt  46801  sge0seq  46804  nnfoctbdjlem  46813  meaiuninc3v  46842  omeiunltfirp  46877  hspdifhsp  46974  hspmbllem2  46985  pimdecfgtioo  47075  pimincfltioo  47076  preimageiingt  47078  preimaleiinlt  47079  smfid  47110  proththd  47974