Theorem adantlrr 708

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  disjxiun  4927  2ndconst  7606  oelim  7963  odi  8008  marypha1lem  8694  dfac12lem2  9366  infunsdom  9436  isf34lem4  9599  distrlem1pr  10247  lcmgcdlem  15809  lcmdvds  15811  drsdirfi  17409  isacs3lem  17637  conjnmzb  18167  psgndif  20451  frlmsslsp  20645  metss2lem  22827  nghmcn  23060  bndth  23268  itg2monolem1  24057  dvmptfsum  24278  ply1divex  24436  itgulm  24702  rpvmasumlem  25768  dchrmusum2  25775  dchrisum0lem2  25799  dchrisum0lem3  25800  mulog2sumlem2  25816  pntibndlem3  25873  wwlksubclwwlk  27584  wwlksubclwwlkOLD  27585  blocni  28362  superpos  29915  chirredlem2  29952  eulerpartlemgvv  31279  ballotlemfc0  31396  ballotlemfcc  31397  bj-finsumval0  34030  pibt2  34139  fin2solem  34319  matunitlindflem1  34329  poimirlem28  34361  heicant  34368  ftc1anclem6  34413  ftc1anc  34416  fdc  34462  incsequz  34465  ismtyres  34528  isdrngo2  34678  rngohomco  34694  keridl  34752  linepsubN  36333  pmapsub  36349  mzpcompact2lem  38743  pellex  38828  monotuz  38934  unxpwdom3  39091  dssmapnvod  39729  radcnvrat  40062  fprodexp  41307  fprodabs2  41308  climxrrelem  41462  dvnprodlem1  41662  stoweidlem34  41751  fourierdlem42  41866  elaa2  41951  sge0iunmptlemfi  42127  aacllem  44270