Theorem 3adantl2 1174

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3ad2antl1  1192  omord2  8499  nnmord  8565  axcc3  10358  lediv2a  12048  zdiv  12597  clatleglb  18482  mulgnn0subcl  19061  mulgsubcl  19062  ghmmulg  19201  obs2ss  21711  scmatf1  22521  neiint  23094  cnpnei  23254  caublcls  25301  axlowdimlem16  29051  clwwlkext2edg  30151  ipval2lem2  30800  fh1  31714  cm2j  31716  hoadddi  31899  hoadddir  31900  lindsadd  37987  lautco  40596  sticksstones1  42638  sticksstones12  42650  supxrge  45790  infleinflem2  45822  stoweidlem44  46494  fourierdlem41  46598  fourierdlem42  46599  fourierdlem54  46610  fourierdlem83  46639  sge0uzfsumgt  46894