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  570  con2b  628  2false  652  pm5.21nii  655  pm4.8  658  imnan  659  notnotnot  663  orcom  682  ioran  704  oridm  709  orbi2i  714  or12  718  pm4.44  731  ordi  765  andi  767  pm4.72  772  oibabs  838  stabtestimpdc  862  pm4.82  896  rnlem  922  3jaob  1238  xoranor  1313  falantru  1339  3impexp  1371  3impexpbicom  1372  alcom  1412  19.26  1415  19.3h  1490  19.3  1491  19.21h  1494  19.43  1564  19.9h  1579  excom  1599  19.41h  1620  19.41  1621  equcom  1639  equsalh  1661  equsex  1663  cbvalh  1683  cbvexh  1685  sbbii  1695  sbh  1706  equs45f  1730  sb6f  1731  sbcof2  1738  sbequ8  1775  sbidm  1779  sb5rf  1780  sb6rf  1781  equvin  1791  sbimv  1821  sbalyz  1923  eu2  1992  eu3h  1993  eu5  1995  mo3h  2001  euan  2004  axext4  2072  cleqh  2187  r19.26  2497  ralcom3  2534  ceqsex  2657  gencbvex  2665  gencbvex2  2666  gencbval  2667  eqvinc  2738  pm13.183  2752  rr19.3v  2753  rr19.28v  2754  reu6  2802  reu3  2803  sbnfc2  2986  difdif  3123  ddifnel  3129  ddifstab  3130  ssddif  3231  difin  3234  uneqin  3248  indifdir  3253  undif3ss  3258  difrab  3271  un00  3326  undifss  3359  ssdifeq0  3361  ralidm  3378  ralf0  3381  ralm  3382  elpr2  3463  snidb  3469  difsnb  3575  preq12b  3609  preqsn  3614  axpweq  3998  exmid0el  4024  exmidel  4025  exmidundif  4026  sspwb  4034  unipw  4035  opm  4052  opth  4055  ssopab2b  4094  elon2  4194  unexb  4258  eusvnfb  4267  eusv2nf  4269  ralxfrALT  4280  uniexb  4286  iunpw  4292  sucelon  4310  unon  4318  sucprcreg  4355  opthreg  4362  ordsuc  4369  dcextest  4386  peano2b  4419  opelxp  4457  opthprc  4477  relop  4574  issetid  4578  elres  4735  iss  4745  issref  4801  xpmlem  4839  ssrnres  4860  dfrel2  4868  relrelss  4944  fn0  5119  funssxp  5165  f00  5186  f0bi  5187  dffo2  5221  ffoss  5269  f1o00  5272  fo00  5273  fv3  5312  dff2  5427  dffo4  5431  dffo5  5432  fmpt  5433  ffnfv  5440  fsn  5453  fsn2  5455  isores1  5575  ssoprab2b  5688  eqfnov2  5734  cnvoprab  5981  reldmtpos  6000  mapsn  6427  mapsncnv  6432  en0  6492  en1  6496  dom0  6534  exmidpw  6604  undifdcss  6613  fidcenum  6644  exmidomni  6777  exmidfodomr  6809  elni2  6852  ltbtwnnqq  6953  enq0ref  6971  elnp1st2nd  7014  elrealeu  7346  elreal2  7347  le2tri3i  7572  elnn0nn  8685  elnnnn0b  8687  elnnnn0c  8688  elnnz  8730  elnn0z  8733  elnnz1  8743  elz2  8788  eluz2b2  9059  elnn1uz2  9063  elioo4g  9321  eluzfz2b  9416  fzm  9421  elfz1end  9438  fzass4  9444  elfz1b  9471  fz01or  9492  nn0fz0  9498  fzolb  9529  fzom  9540  elfzo0  9558  fzo1fzo0n0  9559  elfzo0z  9560  elfzo1  9566  rexanuz  10386  rexuz3  10388  sqrt0rlem  10401  fisum0diag  10798  infssuzex  11038  isprm6  11219  oddpwdclemdc  11244  bdeq  11371  bdop  11423  bdunexb  11468  bj-2inf  11490  bj-nn0suc  11516  exmidsbth  11571
  Copyright terms: Public domain W3C validator