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

Theorem biimparc 293
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 158 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 122 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biantr  894  elrab3t  2749  difprsnss  3532  elpw2g  3939  elon2  4139  ideqg  4515  elrnmpt1s  4612  elrnmptg  4614  fun11iun  5178  eqfnfv2  5298  fmpt  5351  elunirn  5437  spc2ed  5885  tposfo2  5916  tposf12  5918  dom2lem  6319  enfii  6409  ac6sfi  6431  ltexprlemm  6852  elreal2  7061  sizeeqf1oi  9812
  Copyright terms: Public domain W3C validator