Theorem impbid 574

Description: Deduce an equivalence from two implications.

Hypotheses

Ref	Expression
impbid.1	|- (ph -> (ps -> ch))
impbid.2	|- (ph -> (ch -> ps))

Assertion

Ref	Expression
impbid	|- (ph -> (ps <-> ch))

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		dfbi2 572	. 2 |- ((ps <-> ch) <-> ((ps -> ch) /\ (ch -> ps)))
2		impbid.1	. 2 |- (ph -> (ps -> ch))
3		impbid.2	. 2 |- (ph -> (ch -> ps))
4	1, 2, 3	sylanbrc 527	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  impbid1 575  impbid2 576  impbida 577  impcon4bid 578  bitrd 587  pm5.74 643  ibib 650  anbi2d 678  oibabs 716  bibif 745  nbn2 790  orbidi 815  pm5.75 821  pm5.75OLD 822  dedlem0a 834  dedlem0b 836  dedlema 837  dedlemb 839  dedlembOLD 840  orbi1r 1282  albi 1344  exbi 1397  19.21t 1473  equequ1 1494  equequ2 1495  elequ1 1496  elequ2 1497  dral1 1515  cbv2 1524  sbequ12 1545  sbied 1563  sbiedOLD 1564  ax11b 1590  sbequ 1599  sbf3t 1619  sb56 1643  sbal1 1737  eupickb 1836  euor2OLD 1840  2eu2 1854  ceqex 2391  reu6 2443  sbciegft 2482  eqsbc3r 2507  sseq1 2637  reupick 2874  copsexg 3537  sotric 3615  sotrieq 3616  sotrieqOLD 3617  tz7.7 3684  ordsseleqOLD 3688  ordtri1 3693  ordtri1OLD 3694  ordtri3 3697  ordtri3OLD 3698  ordsssuc2OLD 3759  reuuni1OLD 3809  alxfr 3836  ralxfrd 3837  oneqmin 3886  ordsuc 3895  ordelsuc 3900  ordsucelsuc 3902  ordsucelsucOLD 3903  ordunisuc2 3926  limsuc 3933  iss 4254  funssres 4460  tz6.12-1 4693  tz6.12c 4697  ssimaex 4729  eqfnfv 4766  fvimacnv 4778  fsn 4807  fconst2g 4821  fconst5 4824  funiunfv 4842  elunirnALT 4845  f1ocnvfvb 4857  cbvfo 4861  isofr 4879  iotaval 5096  oaord 5228  oawordex 5239  oaordex 5240  oarec 5244  omord2 5246  om00 5254  oeord 5263  erthi 5339  ereldm 5343  pw2en 5505  enen1 5540  enen2 5541  domen1 5542  domen2 5543  sdomen1 5544  sdomen2 5545  domtriord 5546  mapunen 5596  ssenen 5598  nneneq 5606  onomeneq 5612  nndomo 5614  fodomfib 5657  pm54.43 5662  ordiso 5683  hartoglem 5692  ssrankr1 5787  r1pwcl 5798  rankr1b 5810  sbcim2g 5841  omsubsuc2 5878  omsubel 5883  omsubinit 5890  aceq5 5902  carden 5981  carddom 5987  sdomsdomcard 6000  alephord 6023  alephsucdom 6028  indpi 6186  ltexpq 6232  1idpr 6285  ltapr 6303  leltne 6691  ltlen 6692  xrlttri 6727  xrleltne 6733  nnleltp1 7138  nndiv 7143  supxrunb1 7298  supxrunb2 7299  zrevaddcl 7379  zdiv 7397  dfuzi 7414  zmax 7433  zbtwnre 7434  qrevaddcl 7455  flge 7472  modid2 7513  ioo0 7535  elioc2 7558  elico2 7559  elicc2 7560  ioojoin 7585  fzn 7663  fzaddel 7672  elfzp1 7683  fzrevral 7698  expord 7847  hashen 8233  clm4lei 8341  unitg 8893  tgval3 8895  tgss2 8907  clsval2 8961  iscld3 8971  isopn3 8973  elcls3 8987  neips 9003  opnneissb 9004  opnssneib 9005  tpnei 9010  opnneiid 9013  cnpnei 9043  cncnp 9055  sncld 9064  metxp 9111  blssex 9131  neibl 9154  metequiv 9158  metelcls 9243  metcnp4 9248  grpinvf 9364  isga 9450  nvmul0or 9604  nvz 9629  iporthcom 9708  nmobndi 9777  twpar2 10149  elpreima 10161  ficard 10176  cdrci 10182  hausnei2 10222  upxp 10225  txcn 10227  subspid 10249  subcld 10254  subtopmet 10256  fsubbas 10281  fbunfip 10282  fbfgss 10288  hausfillim 10303  elfilmap 10312  elfilmap2 10313  elfilmap3 10314  flimopn 10321  comptoppr 10332  ismnd2 10392  on1el4 10413  uznzr 10416  hvmul0or 10526  his6 10598  hial0 10601  hial02 10602  orthcom 10607  normgt0OLD 10626  normgt0 10627  ocin 10802  shsel3 10912  chssoc 11052  h1de2bi 11110  spansncol 11124  elspansn4 11129  spansnss2 11131  sumspansn 11229  lnopcnbd 11602  lnfncnbd 11629  riesz1 11635  cvcon3 11856  dmdmd 11872  dmdbr3 11877  dmdbr4 11878  dmdbr5 11880  mdslmd1i 11901  atcveq0 11920  chcv1 11927  atssma 11950  atcv0eq 11951  atcv1 11952  bnj145 12477  ghomf1olem 13637  eqreznegel 13654  lbzbi 13657  negdvdsb 13671  dvdsnegb 13672  dvdscmulr 13682  dvdsmulcr 13683  dvdsadd 13688  gcdcllem2 13719  algcvgblem 13745  isprm2lem 13774  coprm 13782  axext4dist 13867  axdenselem8 14026  nndivsub 14258  domrngref 14364  domintreflemb 14366  f1ofi 14376  twsymr 14394  unpde2eg22 14407  injrec2 14466  repcpwti 14503  nZdef 14527  dupre1 14584  inposet 14620  grpdivfo 14737  trran2 14757  rngridfz 14786  svli2 14826  svs2 14829  hmphsym 14883  hmeogrp 14892  subtopsin2 14907  efilcp 14922  efilcp2 14926  rcfpfillem3 14930  fbaslim2 14936  conttnf 14944  iint 15012  trran 15014  cnvtr 15016  lteqtpos 15024  dmrngcmp 15098  ismonc 15163  isepic 15173  isline1 15294  dmsdtriordOLD 15360  elicc3 15362  ccid 15363  elfiun 15369  fictb 15371  inficlALT 15372  ordisoOLD 15374  hartoglemOLD 15383  omsubsuc2OLD 15387  omsubelOLD 15392  omsubinitOLD 15399  opncldf1 15402  opnbnd 15409  cldbnd 15410  opnregcld 15415  cldregopn 15416  opnnei 15417  cncls 15419  cnntr 15420  subsubtop 15423  cnsubsp2 15427  compsub 15431  compfipin0 15436  alexsub 15441  dfcon2 15442  connsub 15443  cnconn 15444  conntoppr 15445  reconn 15451  2ndcsb 15476  isfne3 15482  fnessref 15503  refssfne 15504  locfincomp 15514  locfindsc 15515  comppfsc 15517  neibastop2 15523  ist1-2 15542  ist1-3 15543  isnrm2 15552  fgmin 15558  isufil2 15565  ufprim 15569  uffixfr 15575  filcon 15580  flimcls 15588  cnpfillim 15589  rnelfm 15593  fmfnfmlem4 15597  filfm 15600  flimfbas 15601  fclusnei 15607  fclusbas 15610  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnp 15618  fcluscomp 15621  ufcomp 15622  isfclusf 15625  fclusfnei 15626  filnetlem5 15644  filnet 15645  raleqfn 15672  brabg2 15681  upixp 15729  fzm1 15796  fsum00 15820  subspabs 15840  caushft 15851  iccsplit 15854  ishomeo2 15896  hmeoopn 15899  lmtlm 15908  txsubsp 15912  sstotbnd 15936  totbndbnd 15944  ismtyhmeolem 15950  ismtybnd 15953  heiborlem1 15955  heiborlem10 15964  heiborlem18 15972  grpeqdivid 16038  grpkerinj 16042  isphtpc2 16060  phtpcdm 16061  1idl 16174  0ring 16175  divrngidl 16176  igenval2 16214  ispridlc 16218  isdmn3 16222  impbidd 16227  ersymb2 16258  prtlem16 16272  prtlem18 16279  prter2 16285  prter3 16286  ax10ext 16364  pm14.24 16397  sbiota1 16399  eupickbi 16400  strdif 16719  posasymb 16776  pltval3 16787  lubid 16807  joinle 16820  meetle 16827  lubun 16899  lubunNEW 16900  clatleglb 16903  glb0 16920  oplecon3b 16927  cmtcom 16970  cmtbr3 16975  cmtbr4 16976  cvrnbtwn2 16992  cvrnbtwn3 16993  cvrcon3b 16994  cvrnbtwn4 16996  cvrcmp 16999  atomcvreq0 17010  atomnle 17016  hlexchb 17035  hlatle 17048  hlrelat2 17052  cvr1 17054  cvrexch 17060  atcvr0eq 17064  atcvrj0 17065  atcvrj2b 17069  atltcvr 17072  ps-1 17078  pmaple 17241  paddss 17306  2polcon4b 17331  ispsubcl2 17356

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain