Theorem 3adantl2 1184

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3ad2antl1  1202  omord2  8540  nnmord  8606  axcc3  10410  lediv2a  12100  zdiv  12657  clatleglb  18564  mulgnn0subcl  19144  mulgsubcl  19145  ghmmulg  19289  obs2ss  21839  scmatf1  22649  neiint  23222  cnpnei  23382  caublcls  25429  axlowdimlem16  29216  clwwlkext2edg  30316  ipval2lem2  30965  fh1  31879  cm2j  31881  hoadddi  32064  hoadddir  32065  lindsadd  38124  lautco  40733  sticksstones1  42775  sticksstones12  42787  supxrge  45912  infleinflem2  45944  stoweidlem44  46616  fourierdlem41  46720  fourierdlem42  46721  fourierdlem54  46732  fourierdlem83  46761  sge0uzfsumgt  47016