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

Theorem anandis 805
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
Hypothesis
Ref Expression
anandis.1  |-  ( ( ( ph  /\  ps )  /\  ( ph  /\  ch ) )  ->  ta )
Assertion
Ref Expression
anandis  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ta )

Proof of Theorem anandis
StepHypRef Expression
1 anandis.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ( ph  /\  ch ) )  ->  ta )
21an4s 801 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  ->  ta )
32anabsan 788 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  3impdi  1240  dff13  6007  f1oiso  6074  omord2  6813  fodomacn  7942  ltapi  8785  ltmpi  8786  axpre-ltadd  9047  faclbnd  11586  pwsdiagmhm  14773  tgcl  17039  grpoinvf  21833  ocorth  22798  fh1  23125  fh2  23126  spansncvi  23159  lnopmi  23508  adjlnop  23594  brbtwn2  25849  heicant  26253  mblfinlem2  26256  ismblfin  26259  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anc  26302
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 179  df-an 362
  Copyright terms: Public domain W3C validator