Theorem anandis 678

Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

Hypothesis

Ref	Expression
anandis.1	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏)

Assertion

Ref	Expression
anandis	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Proof of Theorem anandis

Step	Hyp	Ref	Expression
1		anandis.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏)
2	1	an4s 660	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 665	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3impdi  1351  dff13  7197  f1oiso  7294  omord2  8491  fodomacn  9957  ltapi  10804  ltmpi  10805  axpre-ltadd  11068  faclbnd  14207  pwsdiagmhm  18749  tgcl  22894  brbtwn2  28894  grpoinvf  30523  ocorth  31282  fh1  31609  fh2  31610  spansncvi  31643  lnopmi  31991  adjlnop  32077  matunitlindflem2  37667  poimirlem4  37674  heicant  37705  mblfinlem2  37708  ismblfin  37711  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anc  37751