Theorem adantlrr 721

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 482	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 681	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:  disjxiun  5092  2ndconst  8041  oelim  8459  odi  8504  marypha1lem  9342  dfac12lem2  10058  infunsdom  10126  isf34lem4  10290  distrlem1pr  10938  lcmgcdlem  16535  lcmdvds  16537  drsdirfi  18229  isacs3lem  18466  conjnmzb  19150  psgndif  21527  frlmsslsp  21721  metss2lem  24415  nghmcn  24649  bndth  24873  itg2monolem1  25667  dvmptfsum  25895  ply1divex  26058  itgulm  26333  rpvmasumlem  27414  dchrmusum2  27421  dchrisum0lem2  27445  dchrisum0lem3  27446  mulog2sumlem2  27462  pntibndlem3  27519  wwlksubclwwlk  30020  blocni  30767  superpos  32316  chirredlem2  32353  eulerpartlemgvv  34343  ballotlemfc0  34460  ballotlemfcc  34461  bj-finsumval0  37258  pibt2  37390  fin2solem  37585  matunitlindflem1  37595  poimirlem28  37627  heicant  37634  ftc1anclem6  37677  ftc1anc  37680  fdc  37724  incsequz  37727  ismtyres  37787  isdrngo2  37937  rngohomco  37953  keridl  38011  linepsubN  39731  pmapsub  39747  fsuppind  42563  mhpind  42567  mzpcompact2lem  42724  pellex  42808  monotuz  42914  unxpwdom3  43068  cantnfresb  43297  dssmapnvod  43993  radcnvrat  44287  fprodexp  45576  fprodabs2  45577  climxrrelem  45731  dvnprodlem1  45928  stoweidlem34  46016  fourierdlem42  46131  elaa2  46216  sge0iunmptlemfi  46395  aacllem  49787