Theorem 3adantl2 1169

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3ad2antl1  1187  omord2  8495  nnmord  8561  axcc3  10351  lediv2a  12041  zdiv  12590  clatleglb  18475  mulgnn0subcl  19054  mulgsubcl  19055  ghmmulg  19194  obs2ss  21719  scmatf1  22506  neiint  23079  cnpnei  23239  caublcls  25286  axlowdimlem16  29040  clwwlkext2edg  30141  ipval2lem2  30790  fh1  31704  cm2j  31706  hoadddi  31889  hoadddir  31890  lindsadd  37948  lautco  40557  sticksstones1  42599  sticksstones12  42611  supxrge  45786  infleinflem2  45818  stoweidlem44  46490  fourierdlem41  46594  fourierdlem42  46595  fourierdlem54  46606  fourierdlem83  46635  sge0uzfsumgt  46890