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

Theorem anandis 826
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 822 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  ->  ta )
32anabsan 809 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  3impdi  1273  dff13  5971  f1oiso  6042  omord2  7006  fodomacn  8226  ltapi  9072  ltmpi  9073  axpre-ltadd  9334  faclbnd  12066  pwsdiagmhm  15497  tgcl  18574  brbtwn2  23151  grpoinvf  23727  ocorth  24694  fh1  25021  fh2  25022  spansncvi  25055  lnopmi  25404  adjlnop  25490  heicant  28426  mblfinlem2  28429  ismblfin  28432  ftc1anclem6  28472  ftc1anclem7  28473  ftc1anc  28475
  Copyright terms: Public domain W3C validator