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  8577  nnmord  8642  axcc3  10450  lediv2a  12134  zdiv  12661  clatleglb  18526  mulgnn0subcl  19068  mulgsubcl  19069  ghmmulg  19209  obs2ss  21687  scmatf1  22467  neiint  23040  cnpnei  23200  caublcls  25259  axlowdimlem16  28882  clwwlkext2edg  29983  ipval2lem2  30631  fh1  31545  cm2j  31547  hoadddi  31730  hoadddir  31731  lindsadd  37583  lautco  40062  sticksstones1  42105  sticksstones12  42117  supxrge  45313  infleinflem2  45346  stoweidlem44  46021  fourierdlem41  46125  fourierdlem42  46126  fourierdlem54  46137  fourierdlem83  46166  sge0uzfsumgt  46421