ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimparc Unicode version

Theorem biimparc 299
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimparc  |-  ( ( ch  /\  ph )  ->  ps )

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprcd 160 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 124 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biantr  952  elrab3t  2892  difprsnss  3730  elpw2g  4156  elon2  4376  ideqg  4778  elrnmpt1s  4877  elrnmptg  4879  fun11iun  5482  eqfnfv2  5614  fmpt  5666  elunirn  5766  spc2ed  6233  tposfo2  6267  tposf12  6269  dom2lem  6771  enfii  6873  ac6sfi  6897  ltexprlemm  7598  elreal2  7828  fihasheqf1oi  10766  fprod2dlemstep  11629  bastop2  13554
  Copyright terms: Public domain W3C validator