Theorem 3adantl2 1160

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

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

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 1082

This theorem is referenced by:  3ad2antl1  1178  omord2  8050  nnmord  8115  axcc3  9713  lediv2a  11388  zdiv  11906  clatleglb  17569  mulgnn0subcl  18000  mulgsubcl  18001  ghmmulg  18115  obs2ss  20559  scmatf1  20828  neiint  21400  cnpnei  21560  caublcls  23599  axlowdimlem16  26430  clwwlkext2edg  27521  ipval2lem2  28168  fh1  29082  cm2j  29084  hoadddi  29267  hoadddir  29268  lindsadd  34437  lautco  36785  supxrge  41168  infleinflem2  41201  stoweidlem44  41893  fourierdlem41  41997  fourierdlem42  41998  fourierdlem54  42009  fourierdlem83  42038  sge0uzfsumgt  42290