Theorem adantlrl 719

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
adantlrl	⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrl

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 680	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 206  df-an 396

This theorem is referenced by:  1stconst  8105  omlimcl  8598  odi  8599  oelim2  8615  mapxpen  9167  unwdomg  9607  dfac12lem2  10167  infunsdom  10237  fin1a2s  10437  ccatpfx  14683  frlmup1  21731  fbasrn  23787  lmmbr  25185  grporcan  30327  unoplin  31729  hmoplin  31751  superpos  32163  ccatf1  32672  subfacp1lem5  34794  matunitlindflem1  37089  poimirlem4  37097  itg2addnclem  37144  ftc1anclem6  37171  fdc  37218  ismtyres  37281  isdrngo2  37431  rngohomco  37447  rngoisocnv  37454  dssmapnvod  43450  climxrrelem  45137  dvdsn1add  45327  dvnprodlem1  45334  stoweidlem27  45415  fourierdlem97  45591  qndenserrnbllem  45682  sge0iunmptlemfi  45801

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »