ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  impbii GIF 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 (𝜑𝜓)
impbii.2 (𝜓𝜑)
Assertion
Ref Expression
impbii (𝜑𝜓)

Proof of Theorem impbii
StepHypRef Expression
1 impbii.1 . 2 (𝜑𝜓)
2 impbii.2 . 2 (𝜓𝜑)
3 bi3 118 . 2 ((𝜑𝜓) → ((𝜓𝜑) → (𝜑𝜓)))
41, 2, 3mp2 16 1 (𝜑𝜓)
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  577  notnotnot  608  con2b  643  imnan  664  2false  675  pm5.21nii  678  pm4.8  681  oibabs  688  orcom  702  ioran  726  oridm  731  orbi2i  736  or12  740  pm4.44  753  ordi  790  andi  792  pm4.72  797  stdcndc  815  stdcndcOLD  816  stdcn  817  dcnn  818  pm4.82  919  rnlem  945  3jaob  1265  xoranor  1340  falantru  1366  3impexp  1398  3impexpbicom  1399  alcom  1439  19.26  1442  19.3h  1517  19.3  1518  19.21h  1521  19.43  1592  19.9h  1607  excom  1627  19.41h  1648  19.41  1649  equcom  1667  equsalh  1689  equsex  1691  cbvalh  1711  cbvexh  1713  sbbii  1723  sbh  1734  equs45f  1758  sb6f  1759  sbcof2  1766  sbequ8  1803  sbidm  1807  sb5rf  1808  sb6rf  1809  equvin  1819  sbimv  1849  sbalyz  1952  eu2  2021  eu3h  2022  eu5  2024  mo3h  2030  euan  2033  axext4  2101  cleqh  2217  r19.26  2535  ralcom3  2575  ceqsex  2698  gencbvex  2706  gencbvex2  2707  gencbval  2708  eqvinc  2782  pm13.183  2796  rr19.3v  2797  rr19.28v  2798  reu6  2846  reu3  2847  sbnfc2  3030  difdif  3171  ddifnel  3177  ddifstab  3178  ssddif  3280  difin  3283  uneqin  3297  indifdir  3302  undif3ss  3307  difrab  3320  un00  3379  undifss  3413  ssdifeq0  3415  ralidm  3433  ralf0  3436  ralm  3437  elpr2  3519  snidb  3525  difsnb  3633  preq12b  3667  preqsn  3672  axpweq  4065  exmidn0m  4094  exmidsssn  4095  exmid0el  4097  exmidel  4098  exmidundif  4099  exmidundifim  4100  sspwb  4108  unipw  4109  opm  4126  opth  4129  ssopab2b  4168  elon2  4268  unexb  4333  eusvnfb  4345  eusv2nf  4347  ralxfrALT  4358  uniexb  4364  iunpw  4371  sucelon  4389  unon  4397  sucprcreg  4434  opthreg  4441  ordsuc  4448  dcextest  4465  peano2b  4498  opelxp  4539  opthprc  4560  relop  4659  issetid  4663  xpid11  4732  elres  4825  iss  4835  issref  4891  xpmlem  4929  sqxpeq0  4932  ssrnres  4951  dfrel2  4959  relrelss  5035  fn0  5212  funssxp  5262  f00  5284  f0bi  5285  dffo2  5319  ffoss  5367  f1o00  5370  fo00  5371  fv3  5412  dff2  5532  dffo4  5536  dffo5  5537  fmpt  5538  ffnfv  5546  fsn  5560  fsn2  5562  isores1  5683  ssoprab2b  5796  eqfnov2  5846  cnvoprab  6099  reldmtpos  6118  mapsn  6552  mapsncnv  6557  mptelixpg  6596  elixpsn  6597  ixpsnf1o  6598  en0  6657  en1  6661  dom0  6700  exmidpw  6770  undifdcss  6779  fidcenum  6812  djuexb  6897  ctssdc  6966  exmidomni  6982  exmidfodomr  7028  elni2  7090  ltbtwnnqq  7191  enq0ref  7209  elnp1st2nd  7252  elrealeu  7605  elreal2  7606  le2tri3i  7840  elnn0nn  8987  elnnnn0b  8989  elnnnn0c  8990  elnnz  9032  elnn0z  9035  elnnz1  9045  elz2  9090  eluz2b2  9365  elnn1uz2  9369  elioo4g  9685  eluzfz2b  9781  fzm  9786  elfz1end  9803  fzass4  9810  elfz1b  9838  fz01or  9859  nn0fz0  9867  fzolb  9898  fzom  9909  elfzo0  9927  fzo1fzo0n0  9928  elfzo0z  9929  elfzo1  9935  rexanuz  10728  rexuz3  10730  sqrt0rlem  10743  fisum0diag  11178  infssuzex  11569  isprm6  11752  oddpwdclemdc  11778  ennnfone  11865  ctinfom  11868  ctinf  11870  tgclb  12161  xmetunirn  12454  bj-nnsn  12872  bdeq  12948  bdop  13000  bdunexb  13045  bj-2inf  13063  bj-nn0suc  13089  exmidsbth  13146
  Copyright terms: Public domain W3C validator