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  8561  nnmord  8627  axcc3  10440  lediv2a  12127  zdiv  12684  clatleglb  18599  mulgnn0subcl  19184  mulgsubcl  19185  ghmmulg  19329  obs2ss  21916  scmatf1  22725  neiint  23298  cnpnei  23458  caublcls  25505  axlowdimlem16  29344  clwwlkext2edg  30444  ipval2lem2  31093  fh1  32007  cm2j  32009  hoadddi  32192  hoadddir  32193  lindsadd  38305  lautco  40912  sticksstones1  42954  sticksstones12  42966  supxrge  46095  infleinflem2  46127  stoweidlem44  46799  fourierdlem41  46903  fourierdlem42  46904  fourierdlem54  46915  fourierdlem83  46944  sge0uzfsumgt  47199