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  2893  difprsnss  3731  elpw2g  4157  elon2  4377  ideqg  4779  elrnmpt1s  4878  elrnmptg  4880  fun11iun  5483  eqfnfv2  5615  fmpt  5667  elunirn  5767  spc2ed  6234  tposfo2  6268  tposf12  6270  dom2lem  6772  enfii  6874  ac6sfi  6898  ltexprlemm  7599  elreal2  7829  fihasheqf1oi  10767  fprod2dlemstep  11630  bastop2  13587
  Copyright terms: Public domain W3C validator