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  8534  nnmord  8599  axcc3  10398  lediv2a  12084  zdiv  12611  clatleglb  18484  mulgnn0subcl  19026  mulgsubcl  19027  ghmmulg  19167  obs2ss  21645  scmatf1  22425  neiint  22998  cnpnei  23158  caublcls  25216  axlowdimlem16  28891  clwwlkext2edg  29992  ipval2lem2  30640  fh1  31554  cm2j  31556  hoadddi  31739  hoadddir  31740  lindsadd  37614  lautco  40098  sticksstones1  42141  sticksstones12  42153  supxrge  45341  infleinflem2  45374  stoweidlem44  46049  fourierdlem41  46153  fourierdlem42  46154  fourierdlem54  46165  fourierdlem83  46194  sge0uzfsumgt  46449