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  8502  nnmord  8568  axcc3  10360  lediv2a  12050  zdiv  12599  clatleglb  18484  mulgnn0subcl  19063  mulgsubcl  19064  ghmmulg  19203  obs2ss  21709  scmatf1  22496  neiint  23069  cnpnei  23229  caublcls  25276  axlowdimlem16  29026  clwwlkext2edg  30126  ipval2lem2  30775  fh1  31689  cm2j  31691  hoadddi  31874  hoadddir  31875  lindsadd  37934  lautco  40543  sticksstones1  42585  sticksstones12  42597  supxrge  45768  infleinflem2  45800  stoweidlem44  46472  fourierdlem41  46576  fourierdlem42  46577  fourierdlem54  46588  fourierdlem83  46617  sge0uzfsumgt  46872