Theorem anandis 684

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 666	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 671	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  3impdi  1357  dff13  7205  f1oiso  7302  omord2  8499  fodomacn  9976  ltapi  10824  ltmpi  10825  axpre-ltadd  11088  faclbnd  14250  pwsdiagmhm  18797  tgcl  22959  brbtwn2  28999  grpoinvf  30628  ocorth  31387  fh1  31714  fh2  31715  spansncvi  31748  lnopmi  32096  adjlnop  32182  matunitlindflem2  37985  poimirlem4  37992  heicant  38023  mblfinlem2  38026  ismblfin  38029  ftc1anclem6  38066  ftc1anclem7  38067  ftc1anc  38069