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  8488  nnmord  8553  axcc3  10336  lediv2a  12023  zdiv  12549  clatleglb  18426  mulgnn0subcl  19002  mulgsubcl  19003  ghmmulg  19142  obs2ss  21668  scmatf1  22447  neiint  23020  cnpnei  23180  caublcls  25237  axlowdimlem16  28937  clwwlkext2edg  30038  ipval2lem2  30686  fh1  31600  cm2j  31602  hoadddi  31785  hoadddir  31786  lindsadd  37673  lautco  40216  sticksstones1  42259  sticksstones12  42271  supxrge  45461  infleinflem2  45493  stoweidlem44  46166  fourierdlem41  46270  fourierdlem42  46271  fourierdlem54  46282  fourierdlem83  46311  sge0uzfsumgt  46566