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  7252  f1oiso  7349  omord2  8584  fodomacn  10075  ltapi  10922  ltmpi  10923  axpre-ltadd  11186  faclbnd  14313  pwsdiagmhm  18814  tgcl  22912  brbtwn2  28889  grpoinvf  30518  ocorth  31277  fh1  31604  fh2  31605  spansncvi  31638  lnopmi  31986  adjlnop  32072  matunitlindflem2  37646  poimirlem4  37653  heicant  37684  mblfinlem2  37687  ismblfin  37690  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anc  37730