Theorem impbid 519

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		impbid.1	. . 3 |- (ph -> (ps -> ch))
2		impbid.2	. . 3 |- (ph -> (ch -> ps))
3	1, 2	jca 286	. 2 |- (ph -> ((ps -> ch) /\ (ch -> ps)))
4		dfbi2 517	. 2 |- ((ps <-> ch) <-> ((ps -> ch) /\ (ch -> ps)))
5	3, 4	sylibr 198	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  impbid1 520  impbid2 521  impbida 522  bitrd 531  pm5.74 586  ibib 593  anbi2d 619  oibabs 657  bibif 685  nbn2 726  orbidi 748  pm5.75 754  dedlem0b 766  dedlemb 768  19.15 1033  19.18 1086  19.21t 1151  equequ1 1171  equequ2 1172  elequ1 1173  elequ2 1174  dral1 1191  cbv2 1200  sbequ12 1218  sbied 1232  ax11b 1257  sbequ 1266  drsb2 1267  sbf3t 1285  sb56 1304  sbal1 1385  eupickb 1475  euor2 1477  2eu2 1490  ceqex 1932  reu3 1977  sbciegft 2007  reupick 2331  sotric 2939  sotrieq 2940  tz7.7 3001  ordsseleq 3004  ordtri1 3008  ordtri3 3011  ordsssuc2 3060  reuuni1 3106  alxfr 3119  ralxfrd 3120  oneqmin 3162  ordsuc 3171  ordelsuc 3176  ordsucelsuc 3178  ordunisuc2 3198  limsuc 3203  funssres 3657  tz6.12-1 3847  tz6.12c 3851  ssimaex 3879  eqfnfv 3909  fvimacnv 3919  fsn 3948  fconst2g 3959  fconst5 3962  funiunfv 3980  elunirnALT 3983  f1ocnvfvb 3995  cbvfo 3999  isomin 4013  isofr 4016  oaord 4317  oawordex 4327  oaordex 4328  oarec 4332  omord2 4334  om00 4342  oeord 4351  erthi 4421  ereldm 4425  pw2en 4587  enen1 4622  enen2 4623  domen1 4624  domen2 4625  sdomen1 4626  sdomen2 4627  mapunen 4649  ssenen 4651  nneneq 4659  onomeneq 4665  nndomo 4667  fodomfib 4710  pm54.43 4715  ssrankr1 4822  r1pwcl 4833  rankr1b 4845  aceq5 4886  carden 4979  carddom 4985  sdomsdomcard 4998  alephord 5025  alephsucdom 5030  indpi 5188  ltexpq 5234  1idpr 5287  ltapr 5305  leltne 5675  ltlen 5676  xrlttri 5706  xrleltne 5712  lt2msqi 6026  nnleltp1 6100  nndiv 6105  supxrunb1 6257  supxrunb2 6258  zrevaddcl 6338  zdiv 6356  dfuzi 6373  zmax 6392  zbtwnre 6393  qrevaddcl 6414  flge 6431  modid2 6472  ioo0 6494  elioc2 6516  elico2 6517  elicc2 6518  ioojoin 6543  fzn 6621  fzaddel 6630  elfzp1 6641  fzrevral 6650  om2uzlt2i 6662  expord 6799  clm4lei 7284  unitg 7835  tgval3 7837  tgss2 7849  clsval2 7895  iscld3 7905  isopn3 7907  elcls3 7921  neips 7937  opnneissb 7938  opnssneib 7939  tpnei 7944  opnneiid 7947  cncnp 7988  sncld 7997  metxp 8044  blssex 8064  neibl 8087  metequiv 8091  metelcls 8176  metcnp4 8181  grpinvf 8297  nvmul0or 8519  nvz 8544  iporthcom 8623  nmobndi 8692  spwex 8924  hvmul0or 9169  his6 9241  hial0 9244  hial02 9245  orthcom 9250  normgt0OLD 9269  normgt0 9270  ocin 9445  shsel3 9555  chssoc 9695  h1de2bi 9753  spansncol 9767  elspansn4 9772  spansnss2 9774  sumspansn 9872  lnopcnbd 10244  lnfncnbd 10271  riesz1 10277  cvcon3 10492  dmdmd 10508  dmdbr3 10513  dmdbr4 10514  dmdbr5 10516  mdslmd1i 10537  atcveq0 10556  chcv1 10563  atssma 10587  atcv0eq 10588  atcv1 10589  ghomf1olem 10681  nndivsub 10706  domrngref 10764  twpar2 10773  f1ofi 10778  twsymr 10808  unpde2eg22 10826  inposet 10868  lteqtpos 10880  ismnd2 10928  on1el4 10963  uznzr 10967  cdrci 10994  hmphsym 11035  hmeogrp 11044  subtopsin2 11067  efilcp 11083  efilcp2 11087  rcfpfillem3 11091  iint 11157  trran 11159  cnvtr 11161  dmrngcmp 11205  ismonc 11269  isepic 11279  impbid3 11338  dmsdtriord 11408  elicc3 11410  ccid 11412  elfiun 11421  fictb 11423  inficlALT 11424  ordiso 11426  hartoglem 11435  omsubsuc2 11439  omsubel 11444  elomsubsd 11446  omsubinit 11451  opncldf1 11454  opnbnd 11461  cldbnd 11462  opnregcld 11467  cldregopn 11468  opnnei 11469  hausnei2 11471  cnpnei 11472  cncls 11473  cnntr 11474  subspid 11478  subsubtop 11479  subcld 11480  cnsubsp2 11484  compsub 11488  compfipin0 11493  comptoppr 11495  alexsub 11500  dfcon2 11501  connsub 11502  cnconn 11503  conntoppr 11504  subtopmet 11506  reconn 11512  2ndcsb 11537  isfne3 11543  fnessref 11564  refssfne 11565  locfincomp 11575  locfindsc 11576  comppfsc 11578  neibastop2 11584  ist1-2 11603  ist1-3 11604  isnrm2 11613  fsubbas 11630  fbunfip 11631  fgmin 11639  fbfgss 11640  isufil2 11650  ufprim 11654  uffixfr 11660  filcon 11665  flimopn 11679  flimcls 11684  hausfillim 11685  cnpfillim 11686  elfilmap 11690  elfilmap2 11691  elfilmap3 11692  rnelfm 11699  fmfnfmlem4 11703  filfm 11706  flimfbas 11713  fclusnei 11719  fclusbas 11722  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnp 11730  fcluscomp 11733  ufcomp 11734  isfclusf 11737  fclusfnei 11738  filnetlem5 11767  filnet 11768  isga 11772  brabg2 11788  raleqfn 11790  elpreima 11792  upxp 11822  upixp 11823  ficard 11834  fzm1 11867  fsum00 11883  subspabs 11903  metsstop 11909  caushft 11916  iccsplit 11919  ishomeo2 11957  hmeoopn 11960  lmtlm 11969  txcn 11979  txsubsp 11983  sstotbnd 11992  totbndbnd 12000  ismtyhmeolem 12006  ismtybnd 12009  heiborlem1 12011  heiborlem10 12020  heiborlem18 12028  isphtpc2 12102  phtpcdm 12103

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 145  df-an 223

Copyright terms: Public domain