Theorem biimpr 134

Description: Infer a converse implication from a logical equivalence.

Hypothesis

Ref	Expression
biimpr.1	|- (ph <-> ps)

Assertion

Ref	Expression
biimpr	|- (ps -> ph)

Proof of Theorem biimpr

Step	Hyp	Ref	Expression
1		biimpr.1	. 2 |- (ph <-> ps)
2		bi2 131	. 2 |- ((ph <-> ps) -> (ps -> ph))
3	1, 2	ax-mp 6	1 |- (ps -> ph)

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  bicomi 150  bitr 151  imbi2i 160  imbi1i 161  negbii 162  mpbir 165  sylibr 175  sylbir 176  syl5ibr 182  syl6ibr 186  bicon1i 193  pm3.2 232  sylanbr 345  sylan2br 348  anbi2i 367  syl3an1br 625  syl3an2br 626  syl3an3br 627  mpgbir 686  bisb 855  mo2 1026  exmoeu 1039  2euex 1061  eueq2 1429  eueq3 1430  sspss 1569  reuss 1577  neldif 1594  ss0b 1726  pssdifn0 1750  ssunieq 1945  frirr 2176  ordunidif 2260  sucid 2304  unizlim 2364  nnsuc 2389  tfinds 2401  opres 2580  ndmima 2623  fnf 2753  f1o2 2804  f1o00 2823  tz7.44-3 2968  tz7.49 2997  abianfp 3000  f1stres 3096  unblem4 3434  inf3lem3 3466  trcl 3489  kmlem1 3580  ondomcard 3663  ltexpq 3874  suppsr3 4018  axcnre 4087  le2tri3 4311  sqr2irrlem1 4777  znnen 4930  hsupval2t 5301  cmcmlem 5500  sumdmdlem 5786

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

metamath.org