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  585  notbi  655  pm5.21  684  nbn2  686  2falsed  691  pm5.21ndd  694  oibabs  703  orbi2d  779  con4biddc  842  con1bidc  859  con1bdc  863  dedlema  953  dedlemb  954  xorbin  1362  albi  1444  19.21ht  1560  exbi  1583  19.23t  1655  equequ1  1688  equequ2  1689  elequ1  1690  elequ2  1691  equsexd  1707  dral1  1708  cbv2h  1724  sbequ12  1744  sbiedh  1760  drex1  1770  ax11b  1798  sbequ  1812  sbft  1820  sb56  1857  cbvexdh  1898  eupickb  2080  eupickbi  2081  ceqsalt  2712  ceqex  2812  mob2  2864  euxfr2dc  2869  reu6  2873  sbciegft  2939  csbiebt  3039  sseq1  3120  reupick  3360  reupick2  3362  disjeq2  3910  disjeq1  3913  exmidsssnc  4126  copsexg  4166  euotd  4176  poeq2  4222  sotritric  4246  sotritrieq  4247  seeq1  4261  seeq2  4262  alxfr  4382  ralxfrd  4383  rexxfrd  4384  ordelsuc  4421  sosng  4612  iss  4865  iotaval  5099  funeq  5143  funssres  5165  f0dom0  5316  tz6.12c  5451  fnbrfvb  5462  ssimaex  5482  fvimacnv  5535  elpreima  5539  fsn  5592  fconst2g  5635  elunirn  5667  f1ocnvfvb  5681  foeqcnvco  5691  f1eqcocnv  5692  fliftfun  5697  isose  5722  isopo  5724  isoso  5726  f1oiso2  5728  eusvobj2  5760  oprabid  5803  f1opw2  5976  op1steq  6077  rntpos  6154  frecabcl  6296  nnsucelsuc  6387  nnsucsssuc  6388  nnsseleq  6397  nnaord  6405  nnmord  6413  nnaordex  6423  nnawordex  6424  nnm00  6425  erexb  6454  swoord1  6458  swoord2  6459  iinerm  6501  fundmen  6700  mapxpen  6742  ssenen  6745  nneneq  6751  nndomo  6758  fidifsnen  6764  en1eqsnbi  6837  suplub2ti  6888  isoti  6894  ordiso2  6920  ordiso  6921  ctm  6994  ctssdc  6998  enomni  7011  pm54.43  7046  pr2ne  7048  ltexnqq  7223  genprndl  7336  genprndu  7337  nqprl  7366  nqpru  7367  1idprl  7405  1idpru  7406  ltexprlemrnd  7420  ltaprg  7434  recexprlemrnd  7444  cauappcvgprlemrnd  7465  caucvgprlemrnd  7488  caucvgprprlemrnd  7516  suplocexprlemrl  7532  suplocexprlemru  7534  map2psrprg  7620  ltxrlt  7837  lttri3  7851  addlsub  8139  addid0  8142  ltadd2  8188  eqord1  8252  reapti  8348  apreap  8356  ltmul1  8361  apreim  8372  ltleap  8401  mulap0b  8423  apmul1  8555  lt2msq  8651  nnsub  8766  zltnle  9107  zleloe  9108  zrevaddcl  9111  zltp1le  9115  zapne  9132  nn0n0n1ge2b  9137  zdiv  9146  nneo  9161  zeo2  9164  qrevaddcl  9443  npnflt  9605  nmnfgt  9608  xltneg  9626  xleadd1  9665  iccid  9715  zltaddlt1le  9796  fzn  9829  0fz1  9832  uzsplit  9879  fzm1  9887  fzrevral  9892  ssfzo12bi  10009  qltnle  10030  ioo0  10044  ioom  10045  ico0  10046  ioc0  10047  flqge  10062  modqid2  10131  modqmuladd  10146  frec2uzlt2d  10184  shftlem  10595  shftuz  10596  caucvgrelemcau  10759  sqrtsq  10823  abs00ap  10841  cau3lem  10893  maxleb  10995  rexico  11000  negfi  11006  climshft  11080  zsumdc  11160  fsum3  11163  fsum00  11238  dvdsval2  11503  moddvds  11509  negdvdsb  11516  dvdsnegb  11517  dvdscmulr  11529  dvdsmulcr  11530  dvdssub2  11542  fzo0dvdseq  11562  ltoddhalfle  11597  dvdsgcdb  11708  gcdzeq  11717  dvdssqlem  11725  lcmeq0  11759  lcmdvdsb  11772  coprmgcdb  11776  ncoprmgcdne1b  11777  cncongr  11793  isprm2lem  11804  dvdsprime  11810  dvdsprm  11824  coprm  11829  euclemma  11831  rpexp  11838  hashgcdlem  11910  enct  11953  toponcomb  12205  tgss3  12257  isopn3  12304  neiint  12324  neipsm  12333  opnneissb  12334  opnssneib  12335  tpnei  12339  opnneiid  12343  restopnb  12360  tgcn  12387  tgcnp  12388  iscnp4  12397  cnpnei  12398  cnntr  12404  lmss  12425  upxp  12451  txcn  12454  txlm  12458  hmeoopn  12490  hmeocld  12491  xblm  12596  blssexps  12608  blssex  12609  isxms2  12631  neibl  12670  metss  12673  metrest  12685  metcnp3  12690  ivthinclemlr  12794  ivthinclemur  12796  cnplimccntop  12818  subctctexmid  13226  triap  13254
  Copyright terms: Public domain W3C validator