Theorem impbid 195

Description: Deduce an equivalence from two implications. Deduction associated with impbi 191 and impbii 192. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 194. (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

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		impbid.2	. . 3 |- ( ph -> ( ch -> ps ) )
3	1, 2	impbid21d 194	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 49	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 189

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

This theorem depends on definitions:  df-bi 190

This theorem is referenced by:  bicom1  204  impbid1  208  impcon4bid  210  pm5.74  252  imbi1d  323  pm5.501  347  2falsed  357  impbida  848  dedlem0b  970  dedlema  971  dedlemb  972  albi  1701  alexbii  1716  exbiOLD  1728  equequ1  1878  elequ1  1905  elequ2  1912  19.21t  1997  19.23tOLD  2003  sb56  2092  sbequ12  2094  cbv2h  2123  dral1  2170  dral1ALT  2171  ax12b  2189  sbequ  2216  sbft  2219  exsb  2308  eupickb  2378  eupickbi  2379  2eu2  2394  eleq2dOLD  2526  ceqsalt  3082  ceqex  3181  mob2  3230  reu6  3239  sbciegft  3310  eqsbc3r  3336  csbiebt  3395  sseq1  3465  reupick  3739  reupick2  3741  uneqdifeq  3868  eqoreldif  4025  prnebg  4171  disjeq2  4391  disjeq1  4394  disjxiun  4413  disjss3  4415  reusv2lem2  4619  reusv2lem3  4620  alxfr  4627  ralxfrd  4628  copsexg  4701  euotd  4716  poeq2  4778  sotric  4800  sotrieq  4801  freq2  4824  seeq1  4825  seeq2  4826  iss  5171  tz7.7  5468  ordtri1  5475  ordtri3  5478  ordelinel  5540  iotaval  5576  funeq  5620  funssres  5641  f0dom0  5790  tz6.12c  5907  fnbrfvb  5928  ssimaex  5953  fvimacnv  6020  elpreima  6025  eldmrexrnb  6052  fsn  6085  fnsnb  6107  fmptsng  6109  fmptsnd  6110  tpres  6141  fconst2g  6143  fconst5  6146  elunirn  6181  f1ocnvfvb  6203  foeqcnvco  6223  f1eqcocnv  6224  fliftfun  6230  soisores  6243  isofr  6258  isose  6259  isopo  6262  isoso  6264  f1oiso2  6268  eusvobj2  6308  oprabid  6342  f1opw2  6549  oneqmin  6659  ordsuc  6668  ordelsuc  6674  ordsucelsuc  6676  ordunisuc2  6698  limsuc  6703  f1ovv  6791  op1steq  6862  fvn0elsuppb  6959  extmptsuppeq  6966  rntpos  7012  smoiso2  7114  seqomlem2  7194  oaord  7274  oawordex  7284  oaordex  7285  omord2  7294  om00  7302  oeord  7315  nnaord  7346  nnmord  7359  nnawordex  7364  nnaordex  7365  erexb  7414  swoord1  7418  swoord2  7419  iiner  7461  eceqoveq  7494  ralxpmap  7547  omxpenlem  7699  domtriord  7744  mapxpen  7764  mapunen  7767  ssenen  7772  nneneq  7781  onomeneq  7788  nndomo  7792  en1eqsnbi  7828  fodomfib  7877  f1opwfi  7904  fsuppunbi  7930  elfiun  7970  suplub2  8001  ordiso2  8056  ordiso  8057  oieu  8080  brwdom2  8114  brwdom3  8123  cantnflem1  8220  cardidm  8419  carddom2  8437  pm54.43  8460  pr2ne  8462  acnen  8510  acnen2  8512  alephord  8532  alephinit  8552  dfac5  8585  infdif2  8666  fictb  8701  coflim  8717  fincssdom  8779  fin23lem25  8780  isf32lem9  8817  isf34lem4  8833  fin1a2lem11  8866  axdc3lem2  8907  ficard  9016  fpwwe2lem12  9092  fpwwe2  9094  indpi  9358  nqereq  9386  1idpr  9480  ltapr  9496  leltne  9749  ltlen  9761  ltadd2  9764  addlsub  10064  addid0  10067  ltord1  10168  mul0or  10280  ltmul1  10483  mulge0b  10503  lt2msq  10519  negfi  10582  nnsub  10676  nn0sub  10949  zrevaddcl  11011  zltp1le  11015  zdiv  11035  nneo  11048  zeo2  11051  zmax  11290  zbtwnre  11291  qrevaddcl  11315  xrlttri  11467  xrleltne  11473  xralrple  11527  xltneg  11539  xleadd1  11570  xlemul1  11605  supxrunb1  11634  supxrunb2  11635  ioo0  11690  iccid  11710  ico0  11711  ioc0  11712  icc0  11713  difreicc  11793  iccsplit  11794  0fz1  11848  uzsplit  11895  fzm1  11903  fzrevral  11908  ssfzo12bi  12037  elfznelfzob  12046  flge  12073  modid2  12156  ssnn0fi  12229  seqf1olem1  12284  hashen  12562  hashdom  12590  hashle00  12609  hash2exprb  12665  pr2pwpr  12669  hashtpg  12674  reuccats1  12874  ccats1swrdeqbi  12891  repsdf2  12918  scshwfzeqfzo  12962  relexpindlem  13175  shftlem  13180  shftuz  13181  abslt  13426  absle  13427  rexico  13465  cau3lem  13466  rlim2lt  13610  rlim3  13611  o1lo1  13650  rlimdm  13664  climshft  13689  o1dif  13742  isercolllem2  13778  isercoll  13780  zsum  13833  fsum  13835  fsum00  13907  incexclem  13943  zprod  14040  fprod  14044  dvdsval2  14357  moddvds  14361  negdvdsb  14368  dvdsnegb  14369  dvdscmulr  14380  dvdsmulcr  14381  dvdssub2  14391  fzo0dvdseq  14407  bitsf1ocnv  14467  sadcaddlem  14480  bitsuz  14497  dvdsgcdb  14561  gcdeq  14569  dvdssqlem  14576  lcmeq0  14614  lcmdvdsb  14627  lcmfeq0b  14652  lcmf  14655  lcmfdvdsb  14665  isprm2lem  14680  dvdsprime  14686  dvdsprm  14696  coprmgcdb  14703  coprm  14706  euclemma  14714  rpexp  14721  prmdiveq  14783  odzdvds  14789  odzdvdsOLD  14795  pythagtrip  14833  pc2dvds  14877  pcprmpw2  14880  pcprmpw  14881  vdwapun  14973  ramtcl2  15015  ramtcl2OLD  15016  firest  15380  mrieqv2d  15594  isacs2  15608  isssc  15774  setciso  16035  posasymb  16247  pleval2  16260  pltval3  16262  lublecllem  16283  joinle  16309  meetle  16323  lubun  16418  clatleglb  16421  latdisd  16485  letsr  16522  intopsn  16547  gsumval2a  16571  frmdss2  16696  isgrpid2  16751  isgrpinv  16765  symg1bas  17086  oddvdsnn0  17242  oddvds  17245  odeq  17248  odeq1  17260  gexdvds  17284  pgpfi  17306  pgpssslw  17315  fislw  17326  sylow3lem2  17329  lsmelvalm  17352  lsmlub  17364  lsmss1b  17366  lsmss2b  17368  efgs1b  17435  cyggenod  17568  cyggexb  17582  dprdfeq0  17704  unitmulclb  17942  dvreq1  17970  f1rhm0to0  18017  f1rhm0to0ALT  18018  drngmul0or  18045  isabvd  18097  issrngd  18138  lssats2  18272  lspsneq0  18284  lsmelval2  18357  lvecvs0or  18380  lspsneq  18394  lspsneu  18395  lidl1el  18491  lidldvgen  18528  isnzr2  18536  0ringnnzr  18542  0ring01eqbi  18546  rrgeq0  18563  domneq0  18570  ply1coe1eq  18941  cply1coe0bi  18943  znunit  19183  psgndif  19219  ipeq0  19254  ocvsscon  19287  pjdm2  19323  obselocv  19340  islinds4  19442  mat1dimelbas  19545  cramer  19765  unitgOLD  20032  tgss3  20051  clsval2  20114  isopn3  20131  elcls3  20148  opncldf1  20149  neiint  20169  neips  20178  opnneissb  20179  opnssneib  20180  opnnei  20185  tpnei  20186  opnneiid  20191  restcld  20237  restopnb  20240  tgcn  20317  tgcnp  20318  subbascn  20319  iscnp4  20328  cnpnei  20329  cncls2  20338  cncls  20339  cnntr  20340  lmss  20363  hausnei2  20418  lpcls  20429  ordtt1  20444  cmpsub  20464  tgcmp  20465  1stcelcls  20525  locfincmp  20590  kgencn2  20621  ptpjpre1  20635  upxp  20687  txcn  20690  txlm  20712  tgqtop  20776  kqfvima  20794  isr0  20801  regr1lem2  20804  hmeoopn  20830  hmeocld  20831  ptuncnv  20871  fbunfip  20933  fgss2  20938  ufilb  20970  ufprim  20973  trufil  20974  cfinufil  20992  ufildr  20995  elfm2  21012  elfm3  21014  rnelfm  21017  fmfnfmlem4  21021  fmco  21025  flimtopon  21034  flimopn  21039  fbflim2  21041  flimrest  21047  flffbas  21059  cnpflf  21065  fclstopon  21076  fclsnei  21083  fclsbas  21085  fclsfnflim  21091  fclscmp  21094  ufilcmp  21096  isfcf  21098  fcfnei  21099  cnpfcf  21105  alexsubb  21110  alexsubALT  21115  cldsubg  21174  tgphaus  21180  tgpt0  21182  tsmsgsum  21202  tsmsres  21207  xbln0  21478  blssexps  21490  blssex  21491  isxms2  21512  prdsbl  21555  neibl  21565  metss  21572  met2ndc  21587  metrest  21588  metcnp3  21604  nmoeq0  21806  xrsxmet  21876  reconn  21895  iccpnfcnv  22021  fgcfil  22290  iscau4  22298  cfilres  22315  iunmbl2  22559  ismbf3d  22659  mbfaddlem  22665  i1faddlem  22700  i1fmullem  22701  ellimc3  22883  tdeglem4  23058  deg1nn0clb  23088  deg1lt0  23089  dvdsq1p  23160  plypf1  23215  0dgrb  23249  plymul0or  23283  ulmshft  23394  ulmcaulem  23398  ulmcau  23399  cosord  23530  eff1olem  23546  lognegb  23588  eflogeq  23600  logdivlt  23619  efopn  23652  cxpeq0  23672  cxpeq  23746  angpieqvd  23806  dcubic  23821  asinsinb  23872  acoscosb  23873  atantanb  23899  rlimcnp  23940  isppw  24090  isppw2  24091  vmappw  24092  isnsqf  24111  ppieq0  24152  fsumdvdsdiag  24162  dvdsppwf1o  24164  fsumfldivdiag  24168  chpeq0  24185  chteq0  24186  dchrptlem1  24241  lgsdir2lem4  24303  lgsne0  24310  lgsqr  24323  lgsdchrval  24324  lgsquadlem1  24331  m1lgs  24339  iscgrglt  24608  brbtwn  24978  brcgr  24979  brbtwn2  24984  axcontlem7  25049  ausisusgra  25131  nbgraf1olem5  25222  edgusgranbfin  25227  nb3graprlem1  25228  cusgrarn  25236  nbcusgra  25240  cusgrafilem2  25257  uvtxnbgra  25270  uvtxnb  25274  spthonepeq  25366  3v3e3cycl  25442  wlkiswwlk  25475  wlklniswwlkn  25478  wwlknextbi  25502  wwlknredwwlkn0  25504  wwlkextwrd  25505  wwlkextprop  25521  0clwlk  25542  clwlkisclwwlklem0  25565  el2wlkonot  25646  el2spthonot  25647  el2wlkonotot0  25649  el2wlksotot  25659  usg2wlkonot  25660  usg2spthonot  25665  usg2spthonot0  25666  nbhashuvtx  25693  uvtxhashnb  25694  0eusgraiff0rgra  25716  cusgraiffrusgra  25717  eupath2lem3  25756  frgra3vlem2  25778  frgrancvvdeqlem3  25809  numclwwlkun  25856  grpoinvf  26017  rngosn3  26203  rngoueqz  26207  rngoridfz  26212  nvmul0or  26322  nvz  26347  diporthcom  26404  ubthlem3  26563  hvmul0or  26727  his6  26801  hial0  26804  hial02  26805  orthcom  26810  normgt0  26829  ocin  26998  occon3  26999  shsel3  27017  shlub  27116  chssoc  27198  h1de2bi  27256  spansncol  27270  elspansn4  27275  spansnss2  27277  sumspansn  27351  lnopcnbd  27738  lnfncnbd  27759  riesz1  27767  elpjrn  27892  cvcon3  27986  dmdmd  28002  dmdbr3  28007  dmdbr4  28008  dmdbr5  28010  mdslmd1i  28031  atcveq0  28050  chcv1  28057  atssma  28080  atcv0eq  28081  atcv1  28082  bian1d  28149  disjeq1f  28233  br8d  28267  fpwrelmap  28367  xaddeq0  28379  eliccelico  28408  elicoelioo  28409  isarchiofld  28629  unitdivcld  28756  xrge0iifcnv  28788  lmxrge0  28807  indf1ofs  28896  eulerpartlemgh  29260  dstfrvunirn  29356  bnj145OLD  29584  cvmliftmolem2  30054  cvmlift2lem12  30086  mthmb  30268  ghomf1olem  30361  climuzcnv  30364  br8  30445  br6  30446  br4  30447  funbreq  30460  fprb  30462  axext4dist  30496  nodenselem8  30626  dfrdg4  30767  cgrcom  30806  cgrcoml  30812  cgrdegen  30820  btwncom  30830  brsegle  30924  brsegle2  30925  colinbtwnle  30934  btwnoutside  30941  broutsideof3  30942  outsidele  30948  lineunray  30963  lineelsb2  30964  elhf2  30991  elicc3  31022  nn0prpwlem  31027  opnbnd  31030  cldbnd  31031  opnregcld  31035  cldregopn  31036  fnessref  31062  refssfne  31063  neibastop2  31066  fnemeet2  31072  fnejoin2  31074  fgmin  31075  ontgval  31140  ordtop  31145  ordcmp  31156  nndivsub  31166  bj-ssbbi  31280  bj-ssbft  31300  bj-cbv2hv  31377  bj-dral1v  31403  bj-sbftv  31421  bj-equsal1t  31469  bj-19.21t  31477  bj-ceqsalt0  31527  bj-ceqsalt1  31528  bj-xpnzexb  31599  bj-finsumval0  31747  bj-ldiv  31755  bj-bary1  31762  isbasisrelowllem1  31803  isbasisrelowllem2  31804  finxpsuclem  31834  wl-lem-exsb  31940  wl-mo3t  31950  wl-ax11-lem1  31960  poimirlem6  31991  poimirlem7  31992  poimirlem16  32001  poimirlem19  32004  poimirlem22  32007  poimirlem23  32008  poimirlem24  32009  cnambfre  32034  itg2addnc  32041  brabg2  32087  istotbnd3  32148  sstotbnd2  32151  sstotbnd  32152  sstotbnd3  32153  ssbnd  32165  ismtybnd  32184  reheibor  32216  grpoeqdivid  32224  grpokerinj  32228  1idl  32304  0rngo  32305  divrngidl  32306  igenval2  32344  ispridlc  32348  isdmn3  32352  prtlem10  32482  prter2  32498  dral1-o  32519  lshpinN  32600  lsatcveq0  32643  lsatcv0eq  32658  lsatcv1  32659  islshpcv  32664  lkr0f  32705  lkrshp4  32719  lshpkrlem1  32721  lshpset2N  32730  lfl1dim  32732  lfl1dim2N  32733  lub0N  32800  glb0N  32804  oplecon3b  32811  cmtcomN  32860  cmtbr3N  32865  cmtbr4N  32866  cvrnbtwn2  32886  cvrnbtwn3  32887  cvrcon3b  32888  cvrnbtwn4  32890  cvrcmp  32894  atcvreq0  32925  atnle  32928  atlatle  32931  cvlexchb1  32941  cvlcvr1  32950  hlrelat2  33013  exatleN  33014  cvrval3  33023  cvrval4N  33024  cvrexch  33030  atcvr0eq  33036  lnnat  33037  atcvrj0  33038  atcvrj2b  33042  atltcvr  33045  atbtwn  33056  ps-1  33087  3at  33100  islln2a  33127  llncmp  33132  islpln2a  33158  lplncmp  33172  islvol2aN  33202  4at  33223  lvolcmp  33227  pmaple  33371  lncmp  33393  paddss  33455  llnexchb2lem  33478  2polcon4bN  33528  ispsubcl2N  33557  lhpat3  33656  lautcvr  33702  ltrnid  33745  trlval2  33774  trlatn0  33783  ltrnideq  33786  trlnidatb  33788  cdlemeg49lebilem  34151  trlord  34181  cdlemg1a  34182  cdlemg1cex  34200  tendoid0  34437  dva1dim  34597  cdlemm10N  34731  diarnN  34742  cdlemn  34825  dihlspsnssN  34945  dihatexv  34951  dochkrshp  34999  dochkrshp4  35002  djhlsmcl  35027  lcfl6  35113  lcfl8  35115  lcfrvalsnN  35154  lcfrlem9  35163  mapdval2N  35243  mapdordlem2  35250  mapd1o  35261  mapd0  35278  mapdheq2biN  35343  elrfi  35581  diophrw  35646  eldioph2b  35650  diophin  35660  rexrabdioph  35682  rmxycomplete  35810  coprmdvdsb  35882  jm2.19  35893  jm2.26  35902  jm2.27  35908  limsuc2  35944  dgraa0p  36060  rngunsnply  36084  fiuneneq  36116  hashgcdlem  36119  pwelg  36209  isprm7  36704  nzss  36710  dvconstbi  36727  expgrowth  36728  bcc0  36733  axc11next  36801  pm14.24  36827  sbiota1  36829  sbcim2g  36943  sineq0ALT  37374  pwssfi  37419  mapsnd  37514  xralrple2  37615  iccintsng  37662  qinioo  37675  limcresiooub  37761  limclr  37774  dvnmul  37856  dvmptfprodlem  37857  fourierdlem50  38058  fourierdlem89  38097  fourierdlem91  38099  dfsalgen2  38238  sge0repnf  38266  sge0lefi  38278  sge0resplit  38286  sge0fodjrnlem  38296  hspdifhsp  38476  sigarcol  38511  confun  38565  rexsb  38627  2reu2  38646  ralbinrald  38658  rlimdmafv  38717  el1fzopredsuc  38760  mod2eq1n2dvds  38763  iccpartiun  38786  dfodd6  38805  dfeven4  38806  gcdzeq  38831  evensumeven  38872  sgoldbalt  38920  ccats1pfxeqbi  39012  reuccatpfxs1  39015  ralxfrd2  39048  2ffzoeq  39106  uhgrauhgrbi  39209  uhgr0vb  39212  ausgrusgrb  39300  ushgredgedga  39356  ushgredgedgaloop  39358  usgr0vb  39363  usgr1v  39380  nbupgr  39462  nbumgrvtx  39464  nbuhgr2vtx1edgb  39470  edgusgrnbfin  39497  nb3grprlem1  39504  uvtxnbgrb  39524  nbusgrvtxm1uvtx  39528  uvtxnbvtxm1  39529  cusgrfilem2  39567  uhgr0edg0rgrb  39640  cusgrm1rusgr  39648  spthonepeq-av  39784  umgr3v3e3cycl  39925  usgra2pth  39941  uhgrauhgbi  39959  uhg0v  39962  isassintop  40119  uzlidlring  40202  rngciso  40257  rngcisoALTV  40269  ringciso  40308  ringcisoALTV  40332  domnmsuppn0  40427  lindslininds  40530  snlindsntor  40537  isldepslvec2  40551