Theorem 3adant3 599

Description: Deduction adding a conjunct to an antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3

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

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

This theorem is referenced by:  mopick2 1057  itlso 2151  oprabvalig 3048  oaword 3151  ecopoprtrn 3247  eceqopreq 3249  zfregs 3491  ltsopi 3810  ltsopq 3869  genpass 3906  ltsopr 3930  ltsosr 3997  ltasr 4003  ltsor 4055  addcan2t 4123  add12t 4125  addsubasst 4150  addsubt 4151  div23t 4240  ltso 4279  lelttrt 4289  ltaddsub2t 4358  ledivt 4405  ltmuldiv2t 4407  seqrn 4673  hvadd12t 5012  his7 5051  his2subt 5052  projlem26 5218  elspansn2t 5472  spansncol 5473  strlem3a 5693  cvntrt 5724  atexch 5769  atcvatlem 5770  mdsymlem5 5780

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