Theorem 3adant2 598

Description: Deduction adding a conjunct to an antecedent.

Hypothesis

Ref	Expression
3adant.1	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
3adant2	⊢ ((φ ∧ θ ∧ ψ) → χ)

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3simpb 592	. 2 ⊢ ((φ ∧ θ ∧ ψ) → (φ ∧ ψ))
2		3adant.1	. 2 ⊢ ((φ ∧ ψ) → χ)
3	1, 2	syl 12	1 ⊢ ((φ ∧ θ ∧ ψ) → χ)

Syntax hints:   → wi 2   ∧ wa 196   ∧ w3a 581

This theorem is referenced by:  eupickb 1056  oaord 3149  nnaordr 3178  nndi 3180  nnmordi 3188  ecopoprtrn 3247  eceqopreq 3249  ltsopi 3810  ltsopq 3869  ltsopr 3930  ltsosr 3997  ltasr 4003  adddirt 4103  addcan2t 4123  divdiv23t 4271  letrt 4291  ltadd2t 4349  leadd2t 4351  lesub1t 4352  ledivt 4405  uzwo3lem1 4614  infxpidmlem4 4936  hvaddsub12t 5015  his7 5051  his2subt 5052  shlej2t 5357  atcv1 5768  atexch 5769  atcvatlem 5770

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org