Theorem adantlrr 753

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 472	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 681	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  disjxiun  4579  oelim  7501  odi  7546  marypha1lem  8222  dfac12lem2  8849  infunsdom  8919  isf34lem4  9082  distrlem1pr  9726  lcmgcdlem  15157  lcmdvds  15159  drsdirfi  16761  isacs3lem  16989  conjnmzb  17518  psgndif  19767  frlmsslsp  19954  metss2lem  22126  nghmcn  22359  bndth  22565  itg2monolem1  23323  dvmptfsum  23542  ply1divex  23700  itgulm  23966  rpvmasumlem  24976  dchrmusum2  24983  dchrisum0lem2  25007  dchrisum0lem3  25008  mulog2sumlem2  25024  pntibndlem3  25081  3v3e3cycl1  26172  4cycl4v4e  26194  blocni  27044  superpos  28597  chirredlem2  28634  eulerpartlemgvv  29765  ballotlemfc0  29881  ballotlemfcc  29882  bj-finsumval0  32324  fin2solem  32565  matunitlindflem1  32575  poimirlem28  32607  heicant  32614  ftc1anclem6  32660  ftc1anc  32663  fdc  32711  incsequz  32714  ismtyres  32777  isdrngo2  32927  rngohomco  32943  keridl  33001  linepsubN  34056  pmapsub  34072  mzpcompact2lem  36332  pellex  36417  monotuz  36524  unxpwdom3  36683  dssmapnvod  37334  radcnvrat  37535  fprodexp  38661  fprodabs2  38662  dvnprodlem1  38836  stoweidlem34  38927  fourierdlem42  39042  elaa2  39127  sge0iunmptlemfi  39306  wwlksubclwwlks  41232  aacllem  42356