Theorem 3adantl2 1168

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

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

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 1088

This theorem is referenced by:  3ad2antl1  1186  omord2  8492  nnmord  8557  axcc3  10351  lediv2a  12038  zdiv  12565  clatleglb  18443  mulgnn0subcl  18985  mulgsubcl  18986  ghmmulg  19126  obs2ss  21655  scmatf1  22435  neiint  23008  cnpnei  23168  caublcls  25226  axlowdimlem16  28921  clwwlkext2edg  30019  ipval2lem2  30667  fh1  31581  cm2j  31583  hoadddi  31766  hoadddir  31767  lindsadd  37612  lautco  40096  sticksstones1  42139  sticksstones12  42151  supxrge  45338  infleinflem2  45370  stoweidlem44  46045  fourierdlem41  46149  fourierdlem42  46150  fourierdlem54  46161  fourierdlem83  46190  sge0uzfsumgt  46445