Theorem impbid 518

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 288	. 2 |- (ph -> ((ps -> ch) /\ (ch -> ps)))
4		dfbi2 516	. 2 |- ((ps <-> ch) <-> ((ps -> ch) /\ (ch -> ps)))
5	3, 4	sylibr 200	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  impbid1 519  impbid2 520  impbida 521  bitrd 530  pm5.74 585  ibib 592  anbi2d 618  oibabs 656  bibif 683  nbn2 723  orbidi 745  pm5.75 751  dedlem0b 763  dedlemb 765  19.15 999  19.18 1052  19.21t 1117  equequ1 1136  equequ2 1137  elequ1 1138  elequ2 1139  dral1 1156  cbv2 1165  sbequ12 1183  sbied 1197  ax11b 1222  sbequ 1231  drsb2 1232  sb56 1268  sbal1 1348  eupickb 1438  euor2 1440  2eu2 1453  ceqex 1889  reu3 1934  sbciegft 1962  reupick 2282  sotric 2866  sotrieq 2867  reuuni1 2888  alxfr 2902  ralxfrd 2903  tz7.7 2979  ordsseleq 2982  ordtri1 2986  ordtri3 2989  oneqmin 3024  ordsssuc2 3065  ordsuc 3071  ordelsuc 3077  ordsucelsuc 3079  ordunisuc2 3121  limsuc 3126  ssrel 3253  funssres 3558  tz6.12-1 3742  tz6.12c 3746  ssimaex 3774  eqfnfv 3803  fvimacnv 3811  fsn 3840  fconst2g 3851  fconst5 3854  funiunfv 3872  elunirnALT 3875  f1ocnvfvb 3887  cbvfo 3891  isomin 3905  isofr 3908  oaord 4187  oawordex 4197  oaordex 4198  oarec 4202  omord2 4204  om00 4212  oeord 4221  erthi 4287  ereldm 4291  pw2en 4452  enen1 4483  enen2 4484  domen1 4485  domen2 4486  sdomen1 4487  sdomen2 4488  mapunen 4508  ssenen 4510  nneneq 4518  onomeneq 4525  nndomo 4526  pm54.43 4581  ssrankr1 4686  r1pwcl 4697  rankr1b 4709  aceq5 4750  carden 4841  carddom 4846  sdomsdomcard 4859  alephord 4886  alephsucdom 4891  indpi 5046  ltexpq 5092  1idpr 5145  ltapr 5163  leltnet 5533  ltlent 5534  xrlttrit 5564  xrleltnet 5570  lt2msq 5883  nnleltp1t 5956  nndivt 5961  supxrunb1 6091  supxrunb2 6092  zrevaddclt 6172  dfuz 6204  zmax 6222  zbtwnre 6223  flget 6235  qrevaddclt 6276  om2uzlt2 6300  ioo0t 6369  elioc2t 6391  elico2t 6392  elicc2t 6393  ioojoint 6417  fznt 6494  fzaddelt 6501  elfzp1 6511  fzrevralt 6520  expordt 6603  clm4le 7081  unitgt 7622  tgval3t 7624  tgss2t 7636  clsval2 7682  iscld3 7692  isopn3 7694  elcls3 7708  neips 7724  opnneissb 7725  opnssneib 7726  tpnei 7731  opnneiid 7734  cncnp 7775  sncld 7784  metxp 7831  blssex 7851  neibl 7874  metelcls 7962  metcnp4 7967  grpinvf 8075  nvmul0or 8268  nvz 8293  iporthcom 8365  nmobndi 8434  hvmul0ort 8889  his6t 8960  hial0 8963  hial02 8964  orthcom 8969  normgt0tOLD 8988  normgt0t 8989  ocin 9164  shsel3t 9274  chssoct 9414  h1de2b 9472  spansncol 9486  elspansn4t 9491  spansnss2t 9493  sumspansnt 9589  lnopcnbdt 9960  lnfncnbdt 9987  riesz1t 9993  cvcon3t 10206  dmdmdt 10222  dmdbr3 10227  dmdbr4 10228  dmdbr5 10230  mdslmd1 10251  atcveq0 10270  chcv1t 10277  atssmat 10300  atcv0eq 10301  atcv1t 10302  ghomf1olem 10391  nndivsub 10416  inposet 10477  cdrci 10480  hmphsym 10515  hmeogrp 10524  efilcp 10556  efilcp2 10561  rcfpfillem3 10565  iint 10605  trran 10607  ismonc 10713

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 147  df-an 225

Copyright terms: Public domain