Theorem 3adantl2 1211

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3ad2antl1  1216  omord2  7534  nnmord  7599  axcc3  9143  lediv2a  10796  zdiv  11323  clatleglb  16949  mulgnn0subcl  17377  mulgsubcl  17378  ghmmulg  17495  obs2ss  19892  scmatf1  20156  neiint  20718  cnpnei  20878  caublcls  22915  axlowdimlem16  25637  clwwlkext2edg  26330  ipval2lem2  26943  fh1  27861  cm2j  27863  hoadddi  28046  hoadddir  28047  lautco  34401  supxrge  38495  infleinflem2  38528  stoweidlem44  38937  fourierdlem41  39041  fourierdlem42  39042  fourierdlem54  39053  fourierdlem83  39082  sge0uzfsumgt  39337  clwwlksext2edg  41230