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  5095  2ndconst  8043  oelim  8461  odi  8506  marypha1lem  9336  dfac12lem2  10055  infunsdom  10123  isf34lem4  10287  distrlem1pr  10936  lcmgcdlem  16533  lcmdvds  16535  drsdirfi  18228  isacs3lem  18465  conjnmzb  19182  psgndif  21557  frlmsslsp  21751  metss2lem  24455  nghmcn  24689  bndth  24913  itg2monolem1  25707  dvmptfsum  25935  ply1divex  26098  itgulm  26373  rpvmasumlem  27454  dchrmusum2  27461  dchrisum0lem2  27485  dchrisum0lem3  27486  mulog2sumlem2  27502  pntibndlem3  27559  wwlksubclwwlk  30133  blocni  30880  superpos  32429  chirredlem2  32466  eulerpartlemgvv  34533  ballotlemfc0  34650  ballotlemfcc  34651  bj-finsumval0  37486  pibt2  37618  fin2solem  37803  matunitlindflem1  37813  poimirlem28  37845  heicant  37852  ftc1anclem6  37895  ftc1anc  37898  fdc  37942  incsequz  37945  ismtyres  38005  isdrngo2  38155  rngohomco  38171  keridl  38229  linepsubN  40008  pmapsub  40024  fsuppind  42829  mhpind  42833  mzpcompact2lem  42989  pellex  43073  monotuz  43179  unxpwdom3  43333  cantnfresb  43562  dssmapnvod  44257  radcnvrat  44551  fprodexp  45836  fprodabs2  45837  climxrrelem  45989  dvnprodlem1  46186  stoweidlem34  46274  fourierdlem42  46389  elaa2  46474  sge0iunmptlemfi  46653  aacllem  50042