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

Theorem impbii 117
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 112 . 2 ((φψ) → ((ψφ) → (φψ)))
41, 2, 3mp2 16 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  bicom  128  biid  160  2th  163  pm5.74  168  bitri  173  bibi2i  216  bi2.04  237  pm5.4  238  imdi  239  impexp  250  ancom  253  pm4.45im  317  dfbi2  368  anidmOLD  377  anass  383  pm5.32  429  jcab  522  con2b  580  2false  604  pm5.21nii  607  pm4.8  610  imnan  611  notnotnot  615  orcom  634  ioran  656  oridm  661  orbi2i  666  or12  670  pm4.44  683  orabsOLD  715  ordi  717  andi  719  pm4.72  724  oibabs  788  stabtestimpdc  812  pm4.82  843  rnlem  869  3jaob  1181  truanOLD  1244  xoranor  1251  falantru  1275  3impexp  1302  3impexpbicom  1303  alcom  1343  19.26  1346  19.3h  1423  19.3  1424  19.21h  1427  19.43  1497  19.9h  1512  excom  1532  19.41h  1553  19.41  1554  equcom  1571  equsalh  1592  equsex  1594  cbvalh  1614  cbvexh  1616  sbbii  1626  sbh  1637  equs45f  1661  sb6f  1662  sbcof2  1669  sbequ8  1705  sbidm  1709  sb5rf  1710  sb6rf  1711  equvin  1721  sbimv  1751  sbalyz  1853  eu2  1922  eu3h  1923  eu5  1925  mo3h  1931  euan  1934  axext4  2002  cleqh  2115  r19.26  2415  ralcom3  2451  ceqsex  2565  gencbvex  2573  gencbvex2  2574  gencbval  2575  eqvinc  2640  pm13.183  2654  rr19.3v  2655  rr19.28v  2656  reu6  2703  reu3  2704  sbnfc2  2879  difdif  3042  ddifnel  3048  ssddif  3144  difin  3147  uneqin  3161  indifdir  3166  undif3ss  3171  difrab  3184  un00  3236  undifss  3276  ssdifeq0  3278  ralidm  3296  ralf0  3299  ralm  3300  elpr2  3365  snidb  3372  difsnb  3476  preq12b  3511  preqsn  3516  axpweq  3894  sspwb  3922  unipw  3923  opm  3941  opth  3944  ssopab2b  3983  elon2  4058  unexb  4123  eusvnfb  4132  eusv2nf  4134  ralxfrALT  4145  uniexb  4151  iunpw  4157  sucelon  4175  unon  4182  sucprcreg  4207  opthreg  4214  ordsuc  4221  peano2b  4260  opelxp  4297  opthprc  4314  relop  4409  issetid  4413  elres  4569  iss  4577  issref  4630  xpmlem  4667  ssrnres  4686  dfrel2  4694  relrelss  4767  fn0  4940  funssxp  4981  f00  5002  dffo2  5031  ffoss  5079  f1o00  5082  fo00  5083  fv3  5118  dff2  5232  dffo4  5236  dffo5  5237  fmpt  5240  ffnfv  5244  fsn  5256  fsn2  5258  isores1  5375  ssoprab2b  5481  eqfnov2  5527  reldmtpos  5786  elni2  6168  ltbtwnnqq  6266  enq0ref  6282  elnp1st2nd  6324  elreal2  6536  bdeq  7189  bdop  7241  bdunexb  7282  bj-2inf  7299  bj-nn0suc  7321
  Copyright terms: Public domain W3C validator