Theorem anandis 686

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3impdi  1360  dff13  7227  f1oiso  7324  omord2  8524  fodomacn  10002  ltapi  10851  ltmpi  10852  axpre-ltadd  11115  faclbnd  14293  pwsdiagmhm  18841  tgcl  23002  brbtwn2  29045  grpoinvf  30674  ocorth  31433  fh1  31760  fh2  31761  spansncvi  31794  lnopmi  32142  adjlnop  32228  matunitlindflem2  38064  poimirlem4  38071  heicant  38102  mblfinlem2  38105  ismblfin  38108  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anc  38148