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

Theorem anabsi7 793
Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi7.1  |-  ( ps 
->  ( ( ph  /\  ps )  ->  ch )
)
Assertion
Ref Expression
anabsi7  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem anabsi7
StepHypRef Expression
1 anabsi7.1 . . 3  |-  ( ps 
->  ( ( ph  /\  ps )  ->  ch )
)
21anabsi6 792 . 2  |-  ( ( ps  /\  ph )  ->  ch )
32ancoms 440 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  nelrdva  3111  elunii  3988  ordelord  4571  onsucuni2  4781  fvelrn  5833  fnfi  7351  prnmax  8836  fargshiftfo  21586  monotoddzz  26904  oddcomabszz  26905  flcidc  27255  fmul01  27585  stoweidlem4  27628  stoweidlem20  27644  stoweidlem22  27646  stoweidlem27  27651  stoweidlem30  27654  stoweidlem51  27675  stoweidlem59  27683  eel2221  28522
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