Theorem 3adantl2 1186

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3ad2antl1  1204  omord2  8559  nnmord  8625  axcc3  10497  lediv2a  12192  zdiv  12750  clatleglb  18672  mulgnn0subcl  19277  mulgsubcl  19278  ghmmulg  19422  obs2ss  22015  scmatf1  22826  neiint  23402  cnpnei  23562  caublcls  25610  axlowdimlem16  29517  clwwlkext2edg  30629  ipval2lem2  31288  fh1  32202  cm2j  32204  hoadddi  32387  hoadddir  32388  lindsadd  38504  lautco  41122  sticksstones1  43164  sticksstones12  43176  supxrge  46294  infleinflem2  46326  stoweidlem44  46998  fourierdlem41  47102  fourierdlem42  47103  fourierdlem54  47114  fourierdlem83  47143  sge0uzfsumgt  47398