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

Theorem impbii 121
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 116 . 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 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bicom  132  biid  164  2th  167  pm5.74  172  bitri  177  bibi2i  220  bi2.04  241  pm5.4  242  imdi  243  impexp  254  ancom  257  pm4.45im  321  dfbi2  374  anass  387  pm5.32  434  jcab  545  con2b  603  2false  627  pm5.21nii  630  pm4.8  633  imnan  634  notnotnot  638  orcom  657  ioran  679  oridm  684  orbi2i  689  or12  693  pm4.44  706  ordi  740  andi  742  pm4.72  747  oibabs  811  stabtestimpdc  835  pm4.82  868  rnlem  894  3jaob  1208  truanOLD  1277  xoranor  1284  falantru  1310  3impexp  1342  3impexpbicom  1343  alcom  1383  19.26  1386  19.3h  1461  19.3  1462  19.21h  1465  19.43  1535  19.9h  1550  excom  1570  19.41h  1591  19.41  1592  equcom  1609  equsalh  1630  equsex  1632  cbvalh  1652  cbvexh  1654  sbbii  1664  sbh  1675  equs45f  1699  sb6f  1700  sbcof2  1707  sbequ8  1743  sbidm  1747  sb5rf  1748  sb6rf  1749  equvin  1759  sbimv  1789  sbalyz  1891  eu2  1960  eu3h  1961  eu5  1963  mo3h  1969  euan  1972  axext4  2040  cleqh  2153  r19.26  2458  ralcom3  2494  ceqsex  2609  gencbvex  2617  gencbvex2  2618  gencbval  2619  eqvinc  2689  pm13.183  2703  rr19.3v  2704  rr19.28v  2705  reu6  2752  reu3  2753  sbnfc2  2933  difdif  3096  ddifnel  3102  ssddif  3198  difin  3201  uneqin  3215  indifdir  3220  undif3ss  3225  difrab  3238  un00  3290  undifss  3330  ssdifeq0  3332  ralidm  3348  ralf0  3351  ralm  3352  elpr2  3424  snidb  3428  difsnb  3533  preq12b  3568  preqsn  3573  axpweq  3951  sspwb  3979  unipw  3980  opm  3998  opth  4001  ssopab2b  4040  elon2  4140  unexb  4204  eusvnfb  4213  eusv2nf  4215  ralxfrALT  4226  uniexb  4232  iunpw  4238  sucelon  4256  unon  4264  sucprcreg  4300  opthreg  4307  ordsuc  4314  peano2b  4364  opelxp  4401  opthprc  4418  relop  4513  issetid  4517  elres  4673  iss  4681  issref  4734  xpmlem  4771  ssrnres  4790  dfrel2  4798  relrelss  4871  fn0  5045  funssxp  5087  f00  5108  dffo2  5137  ffoss  5185  f1o00  5188  fo00  5189  fv3  5224  dff2  5338  dffo4  5342  dffo5  5343  fmpt  5346  ffnfv  5350  fsn  5362  fsn2  5364  isores1  5481  ssoprab2b  5589  eqfnov2  5635  cnvoprab  5882  reldmtpos  5898  en0  6305  en1  6309  elni2  6469  ltbtwnnqq  6570  enq0ref  6588  elnp1st2nd  6631  elrealeu  6963  elreal2  6964  le2tri3i  7184  elnn0nn  8280  elnnnn0b  8282  elnnnn0c  8283  elnnz  8311  elnn0z  8314  elnnz1  8324  elz2  8369  eluz2b2  8636  elnn1uz2  8640  elioo4g  8903  eluzfz2b  8998  fzm  9003  elfz1end  9020  fzass4  9026  elfz1b  9053  nn0fz0  9079  fzolb  9110  fzom  9121  elfzo0  9139  fzo1fzo0n0  9140  elfzo0z  9141  elfzo1  9147  rexanuz  9814  rexuz3  9816  sqrt0rlem  9829  fz01or  10189  oddpwdclemdc  10240  bdeq  10309  bdop  10361  bdunexb  10406  bj-2inf  10428  bj-nn0suc  10455
  Copyright terms: Public domain W3C validator