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

Theorem anandis 804
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 800 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  ->  ta )
32anabsan 787 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  3impdi  1239  dff13  5971  f1oiso  6038  omord2  6777  fodomacn  7901  ltapi  8744  ltmpi  8745  axpre-ltadd  9006  faclbnd  11544  pwsdiagmhm  14731  tgcl  16997  grpoinvf  21789  ocorth  22754  fh1  23081  fh2  23082  spansncvi  23115  lnopmi  23464  adjlnop  23550  brbtwn2  25756  mblfinlem  26151  ismblfin  26154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator