Theorem 3adantl2 1168

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3adantl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adantl2	⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl2

Step	Hyp	Ref	Expression
1		3simpb 1149	. 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 580	1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  3ad2antl1  1186  omord2  8531  nnmord  8596  axcc3  10391  lediv2a  12077  zdiv  12604  clatleglb  18477  mulgnn0subcl  19019  mulgsubcl  19020  ghmmulg  19160  obs2ss  21638  scmatf1  22418  neiint  22991  cnpnei  23151  caublcls  25209  axlowdimlem16  28884  clwwlkext2edg  29985  ipval2lem2  30633  fh1  31547  cm2j  31549  hoadddi  31732  hoadddir  31733  lindsadd  37607  lautco  40091  sticksstones1  42134  sticksstones12  42146  supxrge  45334  infleinflem2  45367  stoweidlem44  46042  fourierdlem41  46146  fourierdlem42  46147  fourierdlem54  46158  fourierdlem83  46187  sge0uzfsumgt  46442