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  8504  nnmord  8570  axcc3  10360  lediv2a  12048  zdiv  12574  clatleglb  18453  mulgnn0subcl  19029  mulgsubcl  19030  ghmmulg  19169  obs2ss  21696  scmatf1  22487  neiint  23060  cnpnei  23220  caublcls  25277  axlowdimlem16  29042  clwwlkext2edg  30143  ipval2lem2  30791  fh1  31705  cm2j  31707  hoadddi  31890  hoadddir  31891  lindsadd  37858  lautco  40467  sticksstones1  42510  sticksstones12  42522  supxrge  45691  infleinflem2  45723  stoweidlem44  46396  fourierdlem41  46500  fourierdlem42  46501  fourierdlem54  46512  fourierdlem83  46541  sge0uzfsumgt  46796