Theorem impbid 515

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		bi 514	. 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 516  impbid2 517  impbida 518  bitrd 527  pm5.74 582  ibib 589  anbi2d 615  oibabs 653  bibif 680  nbn2 720  orbidi 742  pm5.75 748  dedlem0b 760  dedlemb 762  19.15 995  19.18 1048  19.21t 1113  equequ1 1132  equequ2 1133  elequ1 1134  elequ2 1135  dral1 1152  cbv2 1161  sbequ12 1179  sbied 1193  ax11b 1218  sbequ 1227  drsb2 1228  sb56 1264  sbal1 1344  eupickb 1433  euor2 1435  2eu2 1448  ceqex 1882  reu3 1927  sbciegft 1955  reupick 2275  sotric 2855  sotrieq 2856  reuuni1 2877  alxfr 2891  ralxfrd 2892  tz7.7 2968  ordsseleq 2971  ordtri1 2975  ordtri3 2978  oneqmin 3013  ordsssuc2 3054  ordsuc 3060  ordelsuc 3066  ordsucelsuc 3068  ordunisuc2 3110  limsuc 3115  ssrel 3242  funssres 3544  tz6.12-1 3727  tz6.12c 3731  ssimaex 3759  eqfnfv 3788  fvimacnv 3796  fsn 3825  fconst2g 3836  fconst5 3839  funiunfv 3857  elunirnALT 3860  f1ocnvfvb 3872  cbvfo 3876  isomin 3890  isofr 3893  oaord 4171  oawordex 4181  oaordex 4182  oarec 4186  omord2 4188  om00 4196  oeord 4205  erthi 4271  ereldm 4275  pw2en 4432  enen1 4463  enen2 4464  domen1 4465  domen2 4466  sdomen1 4467  sdomen2 4468  mapunen 4488  ssenen 4490  nneneq 4498  onomeneq 4504  nndomo 4506  fodomfib 4547  pm54.43 4552  ssrankr1 4656  r1pwcl 4667  rankr1b 4679  aceq5 4720  carden 4811  carddom 4816  sdomsdomcard 4828  alephord 4855  alephsucdom 4860  indpi 5014  ltexpq 5060  1idpr 5113  ltapr 5131  leltnet 5502  ltlent 5503  xrlttrit 5533  xrleltnet 5539  lt2msq 5837  nnleltp1t 5909  nndivt 5914  supxrunb1 6044  supxrunb2 6045  zrevaddclt 6125  dfuz 6158  zmax 6176  zbtwnre 6177  flget 6186  qrevaddclt 6221  om2uzlt2 6244  ioo0t 6313  elioc2t 6330  elico2t 6331  elicc2t 6332  fznt 6433  fzaddelt 6440  elfzp1 6450  fzrevralt 6459  expordt 6541  clm4le 7027  unitgt 7573  tgval3t 7575  tgss2t 7587  clsval2 7635  iscld3 7645  isopn3 7647  elcls3 7661  neips 7677  opnneissb 7678  opnssneib 7679  tpnei 7684  opnneiid 7687  cncnp 7728  sncld 7737  metxp 7786  blssex 7806  neibl 7829  metelcls 7916  metcnp4 7920  grpinvf 8029  nvmul0or 8224  nvz 8249  iporthcom 8316  nmobndi 8383  hvmul0ort 8833  his6t 8904  hial0 8907  hial02 8908  orthcom 8913  normgt0tOLD 8932  normgt0t 8933  ocin 9108  shsel3t 9217  chssoct 9357  h1de2b 9415  h1de2bOLD 9416  spansncol 9430  elspansn4t 9436  spansnss2t 9438  sumspansnt 9534  lnopcnbdt 9903  lnfncnbdt 9930  riesz1t 9936  cvcon3t 10149  dmdmdt 10165  dmdbr3 10170  dmdbr4 10171  mdslmd1 10193  atcveq0 10212  chcv1t 10219  atssmat 10242  atcv0eq 10243  atcv1t 10244  ghomf1olem 10330  nndivsub 10357  ompfl2OLD 10363  cdrci 10417  hmphsym 10452  hmeogrp 10461  efilcp 10481  efilcp2 10486  iint 10514  trran 10516  ismonc 10620

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