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  7183  f1oiso  7280  omord2  8477  fodomacn  9939  ltapi  10786  ltmpi  10787  axpre-ltadd  11050  faclbnd  14189  pwsdiagmhm  18731  tgcl  22877  brbtwn2  28876  grpoinvf  30502  ocorth  31261  fh1  31588  fh2  31589  spansncvi  31622  lnopmi  31970  adjlnop  32056  matunitlindflem2  37636  poimirlem4  37643  heicant  37674  mblfinlem2  37677  ismblfin  37680  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anc  37720