Theorem 3adantl2 1167

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

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

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 1089

This theorem is referenced by:  3ad2antl1  1185  omord2  8623  nnmord  8688  axcc3  10507  lediv2a  12189  zdiv  12713  clatleglb  18588  mulgnn0subcl  19127  mulgsubcl  19128  ghmmulg  19268  obs2ss  21772  scmatf1  22558  neiint  23133  cnpnei  23293  caublcls  25362  axlowdimlem16  28990  clwwlkext2edg  30088  ipval2lem2  30736  fh1  31650  cm2j  31652  hoadddi  31835  hoadddir  31836  lindsadd  37573  lautco  40054  sticksstones1  42103  sticksstones12  42115  supxrge  45253  infleinflem2  45286  stoweidlem44  45965  fourierdlem41  46069  fourierdlem42  46070  fourierdlem54  46081  fourierdlem83  46110  sge0uzfsumgt  46365