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

Theorem impbida 561
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 113 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 113 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 127 1  |-  ( ph  ->  ( ps  <->  ch )
)
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-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eqrdav  2081  funfvbrb  5312  f1ocnv2d  5735  1stconst  5873  2ndconst  5874  cnvf1o  5877  ersymb  6186  swoer  6200  erth  6216  enen1  6381  enen2  6382  domen1  6383  domen2  6384  fidifsnen  6405  fundmfibi  6448  f1dmvrnfibi  6452  ordiso2  6505  fzsplit2  9145  fseq1p1m1  9187  elfz2nn0  9205  btwnzge0  9382  modqsubdir  9475  zesq  9688  sizeprg  9832  rereb  9888  abslt  10112  absle  10113  maxleastb  10238  maxltsup  10242  iiserex  10315  dvdsadd2b  10387  nn0ob  10452  dfgcd3  10543  dfgcd2  10547  dvdsmulgcd  10558  lcmgcdeq  10609
  Copyright terms: Public domain W3C validator