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

Theorem impbii 125
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 118 . 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 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:  bicom  139  biid  170  2th  173  pm5.74  178  bitri  183  bibi2i  226  bi2.04  247  pm5.4  248  imdi  249  impexp  261  ancom  264  pm4.45im  332  dfbi2  385  anass  398  pm5.32  448  jcab  592  notnotnot  623  con2b  658  imnan  679  2false  690  pm5.21nii  693  pm4.8  696  oibabs  703  orcom  717  ioran  741  oridm  746  orbi2i  751  or12  755  pm4.44  768  ordi  805  andi  807  pm4.72  812  stdcndc  830  stdcndcOLD  831  stdcn  832  dcnn  833  pm4.82  934  rnlem  960  3jaob  1280  xoranor  1355  falantru  1381  3impexp  1413  3impexpbicom  1414  alcom  1454  19.26  1457  19.3h  1532  19.3  1533  19.21h  1536  19.43  1607  19.9h  1622  excom  1642  19.41h  1663  19.41  1664  equcom  1682  equsalh  1704  equsex  1706  cbvalh  1726  cbvexh  1728  sbbii  1738  sbh  1749  equs45f  1774  sb6f  1775  sbcof2  1782  sbequ8  1819  sbidm  1823  sb5rf  1824  sb6rf  1825  equvin  1835  sbimv  1865  sbalyz  1974  eu2  2043  eu3h  2044  eu5  2046  mo3h  2052  euan  2055  axext4  2123  cleqh  2239  r19.26  2558  ralcom3  2598  ceqsex  2724  gencbvex  2732  gencbvex2  2733  gencbval  2734  eqvinc  2808  pm13.183  2822  rr19.3v  2823  rr19.28v  2824  reu6  2873  reu3  2874  sbnfc2  3060  difdif  3201  ddifnel  3207  ddifstab  3208  ssddif  3310  difin  3313  uneqin  3327  indifdir  3332  undif3ss  3337  difrab  3350  un00  3409  undifss  3443  ssdifeq0  3445  ralidm  3463  ralf0  3466  ralm  3467  elpr2  3549  snidb  3555  difsnb  3663  preq12b  3697  preqsn  3702  axpweq  4095  exmidn0m  4124  exmidsssn  4125  exmid0el  4127  exmidel  4128  exmidundif  4129  exmidundifim  4130  sspwb  4138  unipw  4139  opm  4156  opth  4159  ssopab2b  4198  elon2  4298  unexb  4363  eusvnfb  4375  eusv2nf  4377  ralxfrALT  4388  uniexb  4394  iunpw  4401  sucelon  4419  unon  4427  sucprcreg  4464  opthreg  4471  ordsuc  4478  dcextest  4495  peano2b  4528  opelxp  4569  opthprc  4590  relop  4689  issetid  4693  xpid11  4762  elres  4855  iss  4865  issref  4921  xpmlem  4959  sqxpeq0  4962  ssrnres  4981  dfrel2  4989  relrelss  5065  fn0  5242  funssxp  5292  f00  5314  f0bi  5315  dffo2  5349  ffoss  5399  f1o00  5402  fo00  5403  fv3  5444  dff2  5564  dffo4  5568  dffo5  5569  fmpt  5570  ffnfv  5578  fsn  5592  fsn2  5594  isores1  5715  ssoprab2b  5828  eqfnov2  5878  cnvoprab  6131  reldmtpos  6150  mapsn  6584  mapsncnv  6589  mptelixpg  6628  elixpsn  6629  ixpsnf1o  6630  en0  6689  en1  6693  dom0  6732  exmidpw  6802  undifdcss  6811  fidcenum  6844  djuexb  6929  ctssdc  6998  exmidomni  7014  exmidfodomr  7060  elni2  7129  ltbtwnnqq  7230  enq0ref  7248  elnp1st2nd  7291  elrealeu  7644  elreal2  7645  le2tri3i  7879  elnn0nn  9026  elnnnn0b  9028  elnnnn0c  9029  elnnz  9071  elnn0z  9074  elnnz1  9084  elz2  9129  eluz2b2  9404  elnn1uz2  9408  elioo4g  9724  eluzfz2b  9820  fzm  9825  elfz1end  9842  fzass4  9849  elfz1b  9877  fz01or  9898  nn0fz0  9906  fzolb  9937  fzom  9948  elfzo0  9966  fzo1fzo0n0  9967  elfzo0z  9968  elfzo1  9974  rexanuz  10767  rexuz3  10769  sqrt0rlem  10782  fisum0diag  11217  infssuzex  11649  isprm6  11832  oddpwdclemdc  11858  ennnfone  11945  ctinfom  11948  ctinf  11950  tgclb  12244  xmetunirn  12537  bj-nnsn  12975  bdeq  13051  bdop  13103  bdunexb  13148  bj-2inf  13166  bj-nn0suc  13192  exmidsbth  13249
  Copyright terms: Public domain W3C validator