Theorem adantlrr 734

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantlrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrr

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 694	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:  disjxiun  5104  2ndconst  8102  oelim  8525  odi  8570  marypha1lem  9407  dfac12lem2  10151  infunsdom  10219  isf34lem4  10383  distrlem1pr  11038  lcmgcdlem  16702  lcmdvds  16704  drsdirfi  18399  isacs3lem  18636  conjnmzb  19386  psgndif  21821  frlmsslsp  22015  matunitlindflem1  22907  metss2lem  24743  nghmcn  24977  bndth  25192  itg2monolem1  25984  dvmptfsum  26209  ply1divex  26369  itgulm  26651  rpvmasumlem  27731  dchrmusum2  27738  dchrisum0lem2  27762  dchrisum0lem3  27763  mulog2sumlem2  27779  pntibndlem3  27836  wwlksubclwwlk  30536  blocni  31294  superpos  32843  chirredlem2  32880  eulerpartlemgvv  34895  ballotlemfc0  35012  ballotlemfcc  35013  bj-finsumval0  38045  pibt2  38179  fin2solem  38368  poimirlem28  38405  heicant  38412  ftc1anclem6  38455  ftc1anc  38458  fdc  38503  incsequz  38506  ismtyres  38566  isdrngo2  38716  rngohomco  38732  keridl  38790  linepsubN  40633  pmapsub  40649  fsuppind  43444  mhpind  43448  mzpcompact2lem  43604  pellex  43684  monotuz  43790  unxpwdom3  43944  cantnfresb  44173  dssmapnvod  44868  radcnvrat  45146  fprodexp  46432  fprodabs2  46433  climxrrelem  46585  dvnprodlem1  46782  stoweidlem34  46870  fourierdlem42  46985  elaa2  47070  sge0iunmptlemfi  47249  aacllem  50780