Theorem impbid 397

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 236	. 2 |- (ph -> ((ps -> ch) /\ (ch -> ps)))
4		bi 396	. 2 |- ((ps <-> ch) <-> ((ps -> ch) /\ (ch -> ps)))
5	3, 4	sylibr 175	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  bitrd 406  pm5.74 442  ibib 448  anbi2d 468  pm4.71 481  pm4.72 485  oibabs 493  orbidi 510  mtt 534  tbt 541  nbn 542  biantrud 545  biimt 549  biort 550  bianfd 554  dedlem0a 567  dedlem0b 568  dedlema 569  dedlemb 570  19.15 694  19.18 732  19.33b 771  19.21g 792  a8b 817  eqt2b 818  a13b 819  a14b 820  del34b 837  cbv2 846  del43b 857  sb4b 862  sbequ12 865  sbequ 877  sbied 903  a16gb 934  sbal1 996  eupickb 1056  2eu1 1067  2eu2 1068  2eu3 1069  ceqsalg 1362  cgsex2g 1368  cgsex4g 1369  ceqex 1410  reupick 1578  undif4 1744  elpw2g 1803  elsnc2g 1831  prel12 1875  difex2 1951  reuuni1 1955  iunpw 2040  sotric 2148  sotrieq 2149  tz7.7 2224  ordsseleq 2227  ordtri1 2231  ordtri3 2234  onint0 2262  oneqmin 2273  ord0eln0 2278  onpwsuc 2315  ordsuc 2318  ordelsuc 2322  ordsucelsuc 2324  ordssun 2330  suc11 2341  limsuc 2361  limsssuc 2362  unizlim 2364  dfom2 2374  relss 2480  opres 2580  cores 2659  funssres 2698  imadif 2714  2elresin 2733  f1ocnvb 2812  tz6.12-1 2842  tz6.12c 2846  cleqfv 2880  fvelrn 2883  fsn 2895  f1fv 2916  f1fveq 2918  f1ocnvfvb 2922  cbvfo 2923  isomin 2937  isofr 2940  oaord 3149  oawordex 3159  oaordex 3160  oa00 3161  nnarcl 3174  nnmord 3189  nnmcan 3190  nnaordex 3191  nnawordex 3192  erthi 3218  erth 3219  ereldm 3222  en3d 3304  fundmen 3333  pw2en 3348  sbthbg 3360  enen1 3375  enen2 3376  domen1 3377  domen2 3378  sdomen1 3379  sdomen2 3380  mapunen 3397  ssenen 3399  nneneq 3408  onomeneq 3414  onfin 3415  nndomo 3416  ssrankr1 3520  r1pwcl 3530  aceq5 3563  carden 3638  carddom 3642  sdomsdomcard 3654  cardsdomel 3658  iscard2 3660  alephord 3680  alephsucdom 3685  cardalephex 3691  axrepnd 3740  indpi 3828  ltexpq 3874  ltexpq2 3875  1idpr 3927  ltapr 3945  leltnet 4287  ltlent 4288  add20 4329  lt2sq 4414  nnleltp1t 4448  nndiv 4453  zrevaddclt 4592  elnn0nn 4593  zmax 4618  zbtwnre 4619  flgzt 4626  qrevaddclt 4648  sqr11 4761  infmap2lem2 4952  his6 5057  hial0 5058  hial2eqt 5060  orthcom 5061  normgt0t 5078  ocin 5177  h1de2b 5459  spansncol 5473  elspansn4t 5478  spansnss2t 5480  stge1 5679  stle0 5680  cvcon3t 5716  mdbr3 5729  mdbr4 5730  dmdbr 5731  atsseq 5745  atcveq0 5746  chcv1t 5751  atcv0eq 5767  atcv1 5768  mdsymlem7 5782

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org