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 1150	. 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 580	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  1186  omord2  8605  nnmord  8670  axcc3  10478  lediv2a  12162  zdiv  12688  clatleglb  18563  mulgnn0subcl  19105  mulgsubcl  19106  ghmmulg  19246  obs2ss  21749  scmatf1  22537  neiint  23112  cnpnei  23272  caublcls  25343  axlowdimlem16  28972  clwwlkext2edg  30075  ipval2lem2  30723  fh1  31637  cm2j  31639  hoadddi  31822  hoadddir  31823  lindsadd  37620  lautco  40099  sticksstones1  42147  sticksstones12  42159  supxrge  45349  infleinflem2  45382  stoweidlem44  46059  fourierdlem41  46163  fourierdlem42  46164  fourierdlem54  46175  fourierdlem83  46204  sge0uzfsumgt  46459