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  anass  381  pm5.32  426  jcab  535  con2b  592  2false  616  pm5.21nii  619  pm4.8  622  imnan  623  notnotnot  627  orcom  646  ioran  668  oridm  673  orbi2i  678  or12  682  pm4.44  695  ordi  728  andi  730  pm4.72  735  oibabs  799  stabtestimpdc  823  pm4.82  856  rnlem  882  3jaob  1196  truanOLD  1260  xoranor  1267  falantru  1291  3impexp  1323  3impexpbicom  1324  alcom  1364  19.26  1367  19.3h  1442  19.3  1443  19.21h  1446  19.43  1516  19.9h  1531  excom  1551  19.41h  1572  19.41  1573  equcom  1590  equsalh  1611  equsex  1613  cbvalh  1633  cbvexh  1635  sbbii  1645  sbh  1656  equs45f  1680  sb6f  1681  sbcof2  1688  sbequ8  1724  sbidm  1728  sb5rf  1729  sb6rf  1730  equvin  1740  sbimv  1770  sbalyz  1872  eu2  1941  eu3h  1942  eu5  1944  mo3h  1950  euan  1953  axext4  2021  cleqh  2134  r19.26  2435  ralcom3  2471  ceqsex  2586  gencbvex  2594  gencbvex2  2595  gencbval  2596  eqvinc  2661  pm13.183  2675  rr19.3v  2676  rr19.28v  2677  reu6  2724  reu3  2725  sbnfc2  2900  difdif  3063  ddifnel  3069  ssddif  3165  difin  3168  uneqin  3182  indifdir  3187  undif3ss  3192  difrab  3205  un00  3257  undifss  3297  ssdifeq0  3299  ralidm  3315  ralf0  3318  ralm  3319  elpr2  3386  snidb  3393  difsnb  3497  preq12b  3532  preqsn  3537  axpweq  3915  sspwb  3943  unipw  3944  opm  3962  opth  3965  ssopab2b  4004  elon2  4079  unexb  4143  eusvnfb  4152  eusv2nf  4154  ralxfrALT  4165  uniexb  4171  iunpw  4177  sucelon  4195  unon  4202  sucprcreg  4227  opthreg  4234  ordsuc  4241  peano2b  4280  opelxp  4317  opthprc  4334  relop  4429  issetid  4433  elres  4589  iss  4597  issref  4650  xpmlem  4687  ssrnres  4706  dfrel2  4714  relrelss  4787  fn0  4961  funssxp  5003  f00  5024  dffo2  5053  ffoss  5101  f1o00  5104  fo00  5105  fv3  5140  dff2  5254  dffo4  5258  dffo5  5259  fmpt  5262  ffnfv  5266  fsn  5278  fsn2  5280  isores1  5397  ssoprab2b  5504  eqfnov2  5550  reldmtpos  5809  en0  6211  en1  6215  elni2  6298  ltbtwnnqq  6398  enq0ref  6415  elnp1st2nd  6458  elreal2  6708  le2tri3i  6903  elnn0nn  7980  elnnnn0b  7982  elnnnn0c  7983  elnnz  8011  elnn0z  8014  elnnz1  8024  elz2  8068  eluz2b2  8296  elnn1uz2  8300  elioo4g  8553  eluzfz2b  8647  fzm  8652  elfz1end  8669  fzass4  8675  elfz1b  8702  nn0fz0  8728  fzolb  8759  fzom  8770  elfzo0  8788  fzo1fzo0n0  8789  elfzo0z  8790  elfzo1  8796  sqrt0rlem  9192  bdeq  9258  bdop  9310  bdunexb  9351  bj-2inf  9372  bj-nn0suc  9394
  Copyright terms: Public domain W3C validator