MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anandis Structured version   Visualization version   GIF version

Theorem anandis 675
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
StepHypRef Expression
1 anandis.1 . . 3 (((𝜑𝜓) ∧ (𝜑𝜒)) → 𝜏)
21an4s 657 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) → 𝜏)
32anabsan 662 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜏)
Colors of variables: wff setvar class
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 206  df-an 396
This theorem is referenced by:  3impdi  1349  dff13  7257  f1oiso  7351  omord2  8573  fodomacn  10057  ltapi  10904  ltmpi  10905  axpre-ltadd  11168  faclbnd  14257  pwsdiagmhm  18751  tgcl  22705  brbtwn2  28445  grpoinvf  30067  ocorth  30826  fh1  31153  fh2  31154  spansncvi  31187  lnopmi  31535  adjlnop  31621  matunitlindflem2  36801  poimirlem4  36808  heicant  36839  mblfinlem2  36842  ismblfin  36845  ftc1anclem6  36882  ftc1anclem7  36883  ftc1anc  36885
  Copyright terms: Public domain W3C validator