Theorem 3adantl2 1165

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3ad2antl1  1183  omord2  8360  nnmord  8425  axcc3  10125  lediv2a  11799  zdiv  12320  clatleglb  18151  mulgnn0subcl  18632  mulgsubcl  18633  ghmmulg  18761  obs2ss  20846  scmatf1  21588  neiint  22163  cnpnei  22323  caublcls  24378  axlowdimlem16  27228  clwwlkext2edg  28321  ipval2lem2  28967  fh1  29881  cm2j  29883  hoadddi  30066  hoadddir  30067  lindsadd  35697  lautco  38038  sticksstones1  40030  sticksstones12  40042  supxrge  42767  infleinflem2  42800  stoweidlem44  43475  fourierdlem41  43579  fourierdlem42  43580  fourierdlem54  43591  fourierdlem83  43620  sge0uzfsumgt  43872