Theorem 3adantl2 1180

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 1161	. 2 ⊢ ((𝜑 ∧ 𝜏 ∧ 𝜓) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 589	1 ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3ad2antl1  1198  omord2  8531  nnmord  8597  axcc3  10392  lediv2a  12083  zdiv  12640  clatleglb  18533  mulgnn0subcl  19112  mulgsubcl  19113  ghmmulg  19251  obs2ss  21761  scmatf1  22571  neiint  23144  cnpnei  23304  caublcls  25351  axlowdimlem16  29104  clwwlkext2edg  30204  ipval2lem2  30853  fh1  31767  cm2j  31769  hoadddi  31952  hoadddir  31953  lindsadd  38076  lautco  40685  sticksstones1  42727  sticksstones12  42739  supxrge  45878  infleinflem2  45910  stoweidlem44  46582  fourierdlem41  46686  fourierdlem42  46687  fourierdlem54  46698  fourierdlem83  46727  sge0uzfsumgt  46982