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  7246  f1oiso  7343  omord2  8577  fodomacn  10068  ltapi  10915  ltmpi  10916  axpre-ltadd  11179  faclbnd  14306  pwsdiagmhm  18807  tgcl  22905  brbtwn2  28830  grpoinvf  30459  ocorth  31218  fh1  31545  fh2  31546  spansncvi  31579  lnopmi  31927  adjlnop  32013  matunitlindflem2  37587  poimirlem4  37594  heicant  37625  mblfinlem2  37628  ismblfin  37631  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anc  37671