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

Theorem impbid 128
Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)
Hypotheses
Ref Expression
impbid.1  |-  ( ph  ->  ( ps  ->  ch ) )
impbid.2  |-  ( ph  ->  ( ch  ->  ps ) )
Assertion
Ref Expression
impbid  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid
StepHypRef Expression
1 impbid.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 impbid.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
31, 2impbid21d 127 . 2  |-  ( ph  ->  ( ph  ->  ( ps 
<->  ch ) ) )
43pm2.43i 49 1  |-  ( ph  ->  ( ps  <->  ch )
)
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:  bicom1  130  impbid1  141  pm5.74  178  imbi1d  230  pm5.501  243  pm5.32d  445  impbida  570  notbi  640  pm5.21  669  nbn2  671  2falsed  676  pm5.21ndd  679  oibabs  688  orbi2d  764  con4biddc  827  con1bidc  844  con1bdc  848  dedlema  938  dedlemb  939  xorbin  1347  albi  1429  19.21ht  1545  exbi  1568  19.23t  1640  equequ1  1673  equequ2  1674  elequ1  1675  elequ2  1676  equsexd  1692  dral1  1693  cbv2h  1709  sbequ12  1729  sbiedh  1745  drex1  1754  ax11b  1782  sbequ  1796  sbft  1804  sb56  1841  cbvexdh  1878  eupickb  2058  eupickbi  2059  ceqsalt  2686  ceqex  2786  mob2  2837  euxfr2dc  2842  reu6  2846  sbciegft  2911  csbiebt  3009  sseq1  3090  reupick  3330  reupick2  3332  disjeq2  3880  disjeq1  3883  exmidsssnc  4096  copsexg  4136  euotd  4146  poeq2  4192  sotritric  4216  sotritrieq  4217  seeq1  4231  seeq2  4232  alxfr  4352  ralxfrd  4353  rexxfrd  4354  ordelsuc  4391  sosng  4582  iss  4835  iotaval  5069  funeq  5113  funssres  5135  f0dom0  5286  tz6.12c  5419  fnbrfvb  5430  ssimaex  5450  fvimacnv  5503  elpreima  5507  fsn  5560  fconst2g  5603  elunirn  5635  f1ocnvfvb  5649  foeqcnvco  5659  f1eqcocnv  5660  fliftfun  5665  isose  5690  isopo  5692  isoso  5694  f1oiso2  5696  eusvobj2  5728  oprabid  5771  f1opw2  5944  op1steq  6045  rntpos  6122  frecabcl  6264  nnsucelsuc  6355  nnsucsssuc  6356  nnsseleq  6365  nnaord  6373  nnmord  6381  nnaordex  6391  nnawordex  6392  nnm00  6393  erexb  6422  swoord1  6426  swoord2  6427  iinerm  6469  fundmen  6668  mapxpen  6710  ssenen  6713  nneneq  6719  nndomo  6726  fidifsnen  6732  en1eqsnbi  6805  suplub2ti  6856  isoti  6862  ordiso2  6888  ordiso  6889  ctm  6962  ctssdc  6966  enomni  6979  pm54.43  7014  pr2ne  7016  ltexnqq  7184  genprndl  7297  genprndu  7298  nqprl  7327  nqpru  7328  1idprl  7366  1idpru  7367  ltexprlemrnd  7381  ltaprg  7395  recexprlemrnd  7405  cauappcvgprlemrnd  7426  caucvgprlemrnd  7449  caucvgprprlemrnd  7477  suplocexprlemrl  7493  suplocexprlemru  7495  map2psrprg  7581  ltxrlt  7798  lttri3  7812  addlsub  8100  addid0  8103  ltadd2  8149  eqord1  8213  reapti  8308  apreap  8316  ltmul1  8321  apreim  8332  ltleap  8361  mulap0b  8383  apmul1  8515  lt2msq  8608  nnsub  8723  zltnle  9058  zleloe  9059  zrevaddcl  9062  zltp1le  9066  zapne  9083  nn0n0n1ge2b  9088  zdiv  9097  nneo  9112  zeo2  9115  qrevaddcl  9392  npnflt  9553  nmnfgt  9556  xltneg  9574  xleadd1  9613  iccid  9663  zltaddlt1le  9744  fzn  9777  0fz1  9780  uzsplit  9827  fzm1  9835  fzrevral  9840  ssfzo12bi  9957  qltnle  9978  ioo0  9992  ioom  9993  ico0  9994  ioc0  9995  flqge  10010  modqid2  10079  modqmuladd  10094  frec2uzlt2d  10132  shftlem  10543  shftuz  10544  caucvgrelemcau  10707  sqrtsq  10771  abs00ap  10789  cau3lem  10841  maxleb  10943  rexico  10948  negfi  10954  climshft  11028  zsumdc  11108  fsum3  11111  fsum00  11186  dvdsval2  11408  moddvds  11414  negdvdsb  11421  dvdsnegb  11422  dvdscmulr  11434  dvdsmulcr  11435  dvdssub2  11447  fzo0dvdseq  11467  ltoddhalfle  11502  dvdsgcdb  11613  gcdzeq  11622  dvdssqlem  11630  lcmeq0  11664  lcmdvdsb  11677  coprmgcdb  11681  ncoprmgcdne1b  11682  cncongr  11698  isprm2lem  11709  dvdsprime  11715  dvdsprm  11729  coprm  11734  euclemma  11736  rpexp  11743  hashgcdlem  11814  enct  11857  toponcomb  12106  tgss3  12158  isopn3  12205  neiint  12225  neipsm  12234  opnneissb  12235  opnssneib  12236  tpnei  12240  opnneiid  12244  restopnb  12261  tgcn  12288  tgcnp  12289  iscnp4  12298  cnpnei  12299  cnntr  12305  lmss  12326  upxp  12352  txcn  12355  txlm  12359  hmeoopn  12391  hmeocld  12392  xblm  12497  blssexps  12509  blssex  12510  isxms2  12532  neibl  12571  metss  12574  metrest  12586  metcnp3  12591  ivthinclemlr  12695  ivthinclemur  12697  cnplimccntop  12719  subctctexmid  13092  triap  13120
  Copyright terms: Public domain W3C validator