Theorem adantlrr 757

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 684	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 197  df-an 385

This theorem is referenced by:  disjxiun  4681  oelim  7659  odi  7704  marypha1lem  8380  dfac12lem2  9004  infunsdom  9074  isf34lem4  9237  distrlem1pr  9885  lcmgcdlem  15366  lcmdvds  15368  drsdirfi  16985  isacs3lem  17213  conjnmzb  17742  psgndif  19996  frlmsslsp  20183  metss2lem  22363  nghmcn  22596  bndth  22804  itg2monolem1  23562  dvmptfsum  23783  ply1divex  23941  itgulm  24207  rpvmasumlem  25221  dchrmusum2  25228  dchrisum0lem2  25252  dchrisum0lem3  25253  mulog2sumlem2  25269  pntibndlem3  25326  wwlksubclwwlk  27023  blocni  27788  superpos  29341  chirredlem2  29378  eulerpartlemgvv  30566  ballotlemfc0  30682  ballotlemfcc  30683  bj-finsumval0  33277  fin2solem  33525  matunitlindflem1  33535  poimirlem28  33567  heicant  33574  ftc1anclem6  33620  ftc1anc  33623  fdc  33671  incsequz  33674  ismtyres  33737  isdrngo2  33887  rngohomco  33903  keridl  33961  linepsubN  35356  pmapsub  35372  mzpcompact2lem  37631  pellex  37716  monotuz  37823  unxpwdom3  37982  dssmapnvod  38631  radcnvrat  38830  fprodexp  40144  fprodabs2  40145  climxrrelem  40299  dvnprodlem1  40479  stoweidlem34  40569  fourierdlem42  40684  elaa2  40769  sge0iunmptlemfi  40948  aacllem  42875