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  1349  dff13  7275  f1oiso  7371  omord2  8604  fodomacn  10094  ltapi  10941  ltmpi  10942  axpre-ltadd  11205  faclbnd  14326  pwsdiagmhm  18857  tgcl  22992  brbtwn2  28935  grpoinvf  30561  ocorth  31320  fh1  31647  fh2  31648  spansncvi  31681  lnopmi  32029  adjlnop  32115  matunitlindflem2  37604  poimirlem4  37611  heicant  37642  mblfinlem2  37645  ismblfin  37648  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anc  37688