Theorem anandis 394

Description: Inference that undistributes conjunction in the antecedent.

Hypothesis

Ref	Expression
anandis.1	⊢ (((φ ∧ ψ) ∧ (φ ∧ χ)) → τ)

Assertion

Ref	Expression
anandis	⊢ ((φ ∧ (ψ ∧ χ)) → τ)

Proof of Theorem anandis

Step	Hyp	Ref	Expression
1		anandis.1	. . 3 ⊢ (((φ ∧ ψ) ∧ (φ ∧ χ)) → τ)
2	1	an4s 390	. 2 ⊢ (((φ ∧ φ) ∧ (ψ ∧ χ)) → τ)
3	2	anabsan 386	1 ⊢ ((φ ∧ (ψ ∧ χ)) → τ)

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  3impdi 630  sotrieq 2149  f1fv 2916  f1oiso 2942  oaword 3151  zornlem6 3608  ltapi 3824  ltmpi 3825  distrlem1pr 3921  distrlem4pr 3924  distrlem5pr 3925  ltapr 3945  axltadd 4085  qbtwnre 4650  infxpidmlem1 4933  ocorth 5172  projlem28 5220  shscl 5282  spansncv 5542

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

metamath.org