Theorem impbid 516

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 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 517  impbid2 518  impbida 519  bitrd 528  pm5.74 583  ibib 590  anbi2d 616  oibabs 654  bibif 681  nbn2 721  orbidi 743  pm5.75 749  dedlem0b 761  dedlemb 763  19.15 997  19.18 1050  19.21t 1115  equequ1 1134  equequ2 1135  elequ1 1136  elequ2 1137  dral1 1154  cbv2 1163  sbequ12 1181  sbied 1195  ax11b 1220  sbequ 1229  drsb2 1230  sb56 1266  sbal1 1346  eupickb 1435  euor2 1437  2eu2 1450  ceqex 1886  reu3 1931  sbciegft 1959  reupick 2279  sotric 2860  sotrieq 2861  reuuni1 2882  alxfr 2896  ralxfrd 2897  tz7.7 2973  ordsseleq 2976  ordtri1 2980  ordtri3 2983  oneqmin 3018  ordsssuc2 3059  ordsuc 3065  ordelsuc 3071  ordsucelsuc 3073  ordunisuc2 3115  limsuc 3120  ssrel 3247  funssres 3552  tz6.12-1 3736  tz6.12c 3740  ssimaex 3768  eqfnfv 3797  fvimacnv 3805  fsn 3834  fconst2g 3845  fconst5 3848  funiunfv 3866  elunirnALT 3869  f1ocnvfvb 3881  cbvfo 3885  isomin 3899  isofr 3902  oaord 4181  oawordex 4191  oaordex 4192  oarec 4196  omord2 4198  om00 4206  oeord 4215  erthi 4281  ereldm 4285  pw2en 4446  enen1 4477  enen2 4478  domen1 4479  domen2 4480  sdomen1 4481  sdomen2 4482  mapunen 4502  ssenen 4504  nneneq 4512  onomeneq 4519  nndomo 4521  fodomfibOLD 4567  pm54.43 4572  ssrankr1 4676  r1pwcl 4687  rankr1b 4699  aceq5 4740  carden 4831  carddom 4836  sdomsdomcard 4848  alephord 4875  alephsucdom 4880  indpi 5034  ltexpq 5080  1idpr 5133  ltapr 5151  leltnet 5521  ltlent 5522  xrlttrit 5552  xrleltnet 5558  lt2msq 5881  nnleltp1t 5954  nndivt 5959  supxrunb1 6089  supxrunb2 6090  zrevaddclt 6170  dfuz 6202  zmax 6220  zbtwnre 6221  flget 6233  qrevaddclt 6275  om2uzlt2 6299  ioo0t 6368  elioc2t 6390  elico2t 6391  elicc2t 6392  ioojoint 6416  fznt 6493  fzaddelt 6500  elfzp1 6510  fzrevralt 6519  expordt 6602  mulretOLD 6777  clm4le 7081  unitgt 7623  tgval3t 7625  tgss2t 7637  clsval2 7685  iscld3 7695  isopn3 7697  elcls3 7711  neips 7727  opnneissb 7728  opnssneib 7729  tpnei 7734  opnneiid 7737  cncnp 7778  sncld 7787  metxp 7834  blssex 7854  neibl 7877  metelcls 7965  metcnp4 7970  grpinvf 8079  nvmul0or 8272  nvz 8297  iporthcom 8369  nmobndi 8438  spwpr3OLD 8662  hvmul0ort 8894  his6t 8965  hial0 8968  hial02 8969  orthcom 8974  normgt0tOLD 8993  normgt0t 8994  ocin 9169  shsel3t 9279  chssoct 9419  h1de2b 9477  spansncol 9491  elspansn4t 9496  spansnss2t 9498  sumspansnt 9594  lnopcnbdt 9965  lnfncnbdt 9992  riesz1t 9998  cvcon3t 10211  dmdmdt 10227  dmdbr3 10232  dmdbr4 10233  dmdbr5 10235  mdslmd1 10256  atcveq0 10275  chcv1t 10282  atssmat 10305  atcv0eq 10306  atcv1t 10307  ghomf1olem 10396  nndivsub 10421  cdrci 10494  hmphsym 10529  hmeogrp 10538  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  rcfpfillem3 10589  rcfpfillem3OLD 10590  iint 10634  trran 10636  ismonc 10742

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