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

Theorem impbida 585
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
Hypotheses
Ref Expression
impbida.1  |-  ( (
ph  /\  ps )  ->  ch )
impbida.2  |-  ( (
ph  /\  ch )  ->  ps )
Assertion
Ref Expression
impbida  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbida
StepHypRef Expression
1 impbida.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 114 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 114 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 128 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eqrdav  2138  funfvbrb  5533  f1ocnv2d  5974  1stconst  6118  2ndconst  6119  cnvf1o  6122  ersymb  6443  swoer  6457  erth  6473  enen1  6734  enen2  6735  domen1  6736  domen2  6737  xpmapenlem  6743  fidifsnen  6764  fundmfibi  6827  f1dmvrnfibi  6832  ordiso2  6920  fzsplit2  9837  fseq1p1m1  9881  elfz2nn0  9899  btwnzge0  10080  modqsubdir  10173  zesq  10417  hashprg  10561  rereb  10642  abslt  10867  absle  10868  maxleastb  10993  maxltsup  10997  xrltmaxsup  11033  xrmaxltsup  11034  iserex  11115  mptfzshft  11218  fsumrev  11219  dvdsadd2b  11546  nn0ob  11611  dfgcd3  11704  dfgcd2  11708  dvdsmulgcd  11719  lcmgcdeq  11770  qden1elz  11889  cncnp  12408  xmetxpbl  12686  dedekindicc  12789  coseq0q4123  12931  coseq0negpitopi  12933  relogeftb  12960  pwf1oexmid  13247  isomninnlem  13278  apdiff  13292
  Copyright terms: Public domain W3C validator