Theorem impbid2 518

Description: Infer an equivalence from two implications.

Hypotheses

Ref	Expression
impbid2.1	|- (ps -> ch)
impbid2.2	|- (ph -> (ch -> ps))

Assertion

Ref	Expression
impbid2	|- (ph -> (ps <-> ch))

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.1	. . 3 |- (ps -> ch)
2	1	a1i 8	. 2 |- (ph -> (ps -> ch))
3		impbid2.2	. 2 |- (ph -> (ch -> ps))
4	2, 3	impbid 516	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm4.72 641  mtt 712  biimt 731  biort 734  dedlem0a 760  dedlema 762  19.23t 1116  cgsexg 1831  cgsex2g 1832  cgsex4g 1833  elab3g 1902  abidhb 1912  hbsbc1gd 1983  hbsbcgd 1984  uniiunlem 2132  elsnc2g 2436  eqsn 2474  prel12 2484  intmin4 2559  elpw2g 2727  opelopab2 2819  difex2 2877  ord0eln0 3023  ordpwsuc 3066  ordunisuc2 3115  limsssuc 3121  dfom2 3133  opres 3375  cores 3499  relcnvexb 3521  f1ocnvb 3702  fnoprabg 4012  omord 4199  nneob 4255  pw2en 4446  sbthbg 4458  ltexpq2 5081  nltpnftt 5566  ngtmnftt 5567  xrrebndt 5568  supxrre 6083  elnn0nn 6171  iccnegt 6407  fz1sbct 6517  reim0bt 6775  clm3 7079  bastopt 7633  0top 7635  bastop 7642  subtop 7646  neiint 7719  islp2 7747  hmopadj2t 9865  mdslle1 10244  mdslle2 10245  elghomlem2 10383

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