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  7229  f1oiso  7326  omord2  8531  fodomacn  10009  ltapi  10856  ltmpi  10857  axpre-ltadd  11120  faclbnd  14255  pwsdiagmhm  18758  tgcl  22856  brbtwn2  28832  grpoinvf  30461  ocorth  31220  fh1  31547  fh2  31548  spansncvi  31581  lnopmi  31929  adjlnop  32015  matunitlindflem2  37611  poimirlem4  37618  heicant  37649  mblfinlem2  37652  ismblfin  37655  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anc  37695