Theorem impbid2 521

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 519	1 |- (ph -> (ps <-> ch))

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

This theorem is referenced by:  pm4.72 644  mtt 717  biimt 736  biort 739  dedlem0a 765  dedlema 767  19.23t 1152  cgsexg 1877  cgsex2g 1878  cgsex4g 1879  elab3g 1948  abidhb 1958  hbsbc1gd 2031  hbsbcgd 2032  uniiunlem 2184  elsnc2g 2497  eqsn 2539  prel12 2549  intmin4 2626  elpw2g 2801  opelopab2 2896  ord0eln0 3027  difex2 3101  ordpwsuc 3172  ordunisuc2 3198  limsssuc 3204  dfom2 3220  ssrel 3334  ssrelrel 3340  opres 3462  cores 3602  relcnvexb 3626  f1ocnvb 3810  fvopab6 3905  eqfnfv2 3911  fnoprabg 4072  omord 4335  nneob 4395  pw2en 4587  sbthbg 4603  ltexpq2 5235  nltpnft 5720  ngtmnft 5721  xrrebnd 5722  rpneg 6211  supxrre 6251  elnn0nn 6339  iccneg 6534  fz1sbc 6648  reim0b 6976  clm3i 7282  bastop 7845  0top 7847  bastop1 7854  subtop 7858  neiint 7929  islp2 7957  hmopadj2 10145  mdslle1i 10525  mdslle2i 10526  elghomlem2 10668  domintref 10767  dupos2 10879  iepiclem 11278  dfiin2g 11400  dfcon2 11501  comppfsc 11578  ufileu 11658  fzsn 11865  absz 11868  negmod0 11872  cnresima 11952  isbnd3 11997  heiborlem28 12038  rrntotbnd 12078

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 145  df-an 223

Copyright terms: Public domain