Theorem adantlrr 733

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 487	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 693	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:  disjxiun  5102  2ndconst  8084  oelim  8507  odi  8552  marypha1lem  9381  dfac12lem2  10116  infunsdom  10184  isf34lem4  10349  distrlem1pr  10998  lcmgcdlem  16654  lcmdvds  16656  drsdirfi  18351  isacs3lem  18588  conjnmzb  19314  psgndif  21712  frlmsslsp  21906  metss2lem  24629  nghmcn  24863  bndth  25078  itg2monolem1  25870  dvmptfsum  26095  ply1divex  26255  itgulm  26529  rpvmasumlem  27609  dchrmusum2  27616  dchrisum0lem2  27640  dchrisum0lem3  27641  mulog2sumlem2  27657  pntibndlem3  27714  wwlksubclwwlk  30318  blocni  31066  superpos  32615  chirredlem2  32652  eulerpartlemgvv  34683  ballotlemfc0  34800  ballotlemfcc  34801  bj-finsumval0  37789  pibt2  37923  fin2solem  38117  matunitlindflem1  38127  poimirlem28  38159  heicant  38166  ftc1anclem6  38209  ftc1anc  38212  fdc  38256  incsequz  38259  ismtyres  38319  isdrngo2  38469  rngohomco  38485  keridl  38543  linepsubN  40388  pmapsub  40404  fsuppind  43184  mhpind  43188  mzpcompact2lem  43344  pellex  43424  monotuz  43530  unxpwdom3  43684  cantnfresb  43913  dssmapnvod  44608  radcnvrat  44888  fprodexp  46168  fprodabs2  46169  climxrrelem  46321  dvnprodlem1  46518  stoweidlem34  46606  fourierdlem42  46721  elaa2  46806  sge0iunmptlemfi  46985  aacllem  50430