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

Theorem anandis 828
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 824 . 2  |-  ( ( ( ph  /\  ph )  /\  ( ps  /\  ch ) )  ->  ta )
32anabsan 811 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  1283  dff13  6165  f1oiso  6246  omord2  7228  fodomacn  8449  ltapi  9293  ltmpi  9294  axpre-ltadd  9556  faclbnd  12348  pwsdiagmhm  15871  tgcl  19337  brbtwn2  24040  grpoinvf  25073  ocorth  26040  fh1  26367  fh2  26368  spansncvi  26401  lnopmi  26750  adjlnop  26836  heicant  29983  mblfinlem2  29986  ismblfin  29989  ftc1anclem6  30029  ftc1anclem7  30030  ftc1anc  30032
  Copyright terms: Public domain W3C validator