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  8482  nnmord  8547  axcc3  10326  lediv2a  12013  zdiv  12540  clatleglb  18421  mulgnn0subcl  18997  mulgsubcl  18998  ghmmulg  19138  obs2ss  21664  scmatf1  22444  neiint  23017  cnpnei  23177  caublcls  25234  axlowdimlem16  28933  clwwlkext2edg  30031  ipval2lem2  30679  fh1  31593  cm2j  31595  hoadddi  31778  hoadddir  31779  lindsadd  37652  lautco  40135  sticksstones1  42178  sticksstones12  42190  supxrge  45376  infleinflem2  45408  stoweidlem44  46081  fourierdlem41  46185  fourierdlem42  46186  fourierdlem54  46197  fourierdlem83  46226  sge0uzfsumgt  46481