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

Theorem impbii 124
Description: Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
impbii.1  |-  ( ph  ->  ps )
impbii.2  |-  ( ps 
->  ph )
Assertion
Ref Expression
impbii  |-  ( ph  <->  ps )

Proof of Theorem impbii
StepHypRef Expression
1 impbii.1 . 2  |-  ( ph  ->  ps )
2 impbii.2 . 2  |-  ( ps 
->  ph )
3 bi3 117 . 2  |-  ( (
ph  ->  ps )  -> 
( ( ps  ->  ph )  ->  ( ph  <->  ps ) ) )
41, 2, 3mp2 16 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  bicom  138  biid  169  2th  172  pm5.74  177  bitri  182  bibi2i  225  bi2.04  246  pm5.4  247  imdi  248  impexp  259  ancom  262  pm4.45im  327  dfbi2  380  anass  393  pm5.32  441  jcab  568  con2b  626  2false  650  pm5.21nii  653  pm4.8  656  imnan  657  notnotnot  661  orcom  680  ioran  702  oridm  707  orbi2i  712  or12  716  pm4.44  729  ordi  763  andi  765  pm4.72  770  oibabs  834  stabtestimpdc  858  pm4.82  892  rnlem  918  3jaob  1234  xoranor  1309  falantru  1335  3impexp  1367  3impexpbicom  1368  alcom  1408  19.26  1411  19.3h  1486  19.3  1487  19.21h  1490  19.43  1560  19.9h  1575  excom  1595  19.41h  1616  19.41  1617  equcom  1635  equsalh  1656  equsex  1658  cbvalh  1678  cbvexh  1680  sbbii  1690  sbh  1701  equs45f  1725  sb6f  1726  sbcof2  1733  sbequ8  1770  sbidm  1774  sb5rf  1775  sb6rf  1776  equvin  1786  sbimv  1816  sbalyz  1918  eu2  1987  eu3h  1988  eu5  1990  mo3h  1996  euan  1999  axext4  2067  cleqh  2182  r19.26  2491  ralcom3  2527  ceqsex  2647  gencbvex  2655  gencbvex2  2656  gencbval  2657  eqvinc  2727  pm13.183  2741  rr19.3v  2742  rr19.28v  2743  reu6  2791  reu3  2792  sbnfc2  2972  difdif  3108  ddifnel  3114  ddifstab  3115  ssddif  3215  difin  3218  uneqin  3232  indifdir  3237  undif3ss  3242  difrab  3255  un00  3307  undifss  3340  ssdifeq0  3342  ralidm  3359  ralf0  3362  ralm  3363  elpr2  3439  snidb  3443  difsnb  3549  preq12b  3583  preqsn  3588  axpweq  3966  exmid0el  3990  exmidel  3991  exmidundif  3992  sspwb  4000  unipw  4001  opm  4018  opth  4021  ssopab2b  4060  elon2  4160  unexb  4224  eusvnfb  4233  eusv2nf  4235  ralxfrALT  4246  uniexb  4252  iunpw  4258  sucelon  4276  unon  4284  sucprcreg  4321  opthreg  4328  ordsuc  4335  peano2b  4384  opelxp  4421  opthprc  4438  relop  4535  issetid  4539  elres  4695  iss  4705  issref  4758  xpmlem  4795  ssrnres  4814  dfrel2  4822  relrelss  4895  fn0  5070  funssxp  5112  f00  5133  dffo2  5163  ffoss  5211  f1o00  5214  fo00  5215  fv3  5251  dff2  5365  dffo4  5369  dffo5  5370  fmpt  5373  ffnfv  5377  fsn  5389  fsn2  5391  isores1  5507  ssoprab2b  5615  eqfnov2  5661  cnvoprab  5908  reldmtpos  5924  en0  6365  en1  6369  undifdcss  6469  exmidomni  6583  elni2  6643  ltbtwnnqq  6744  enq0ref  6762  elnp1st2nd  6805  elrealeu  7137  elreal2  7138  le2tri3i  7363  elnn0nn  8474  elnnnn0b  8476  elnnnn0c  8477  elnnz  8519  elnn0z  8522  elnnz1  8532  elz2  8577  eluz2b2  8848  elnn1uz2  8852  elioo4g  9110  eluzfz2b  9205  fzm  9210  elfz1end  9227  fzass4  9233  elfz1b  9260  fz01or  9281  nn0fz0  9287  fzolb  9316  fzom  9327  elfzo0  9345  fzo1fzo0n0  9346  elfzo0z  9347  elfzo1  9353  rexanuz  10100  rexuz3  10102  sqrt0rlem  10115  infssuzex  10577  isprm6  10758  oddpwdclemdc  10783  bdeq  10906  bdop  10958  bdunexb  11003  bj-2inf  11025  bj-nn0suc  11051
  Copyright terms: Public domain W3C validator