Theorem biimpr 152

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 149	. 2 |- ((ph <-> ps) -> (ps -> ph))
3	1, 2	ax-mp 7	1 |- (ps -> ph)

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

This theorem is referenced by:  bicomi 172  bitr 173  imbi2i 185  imbi1i 186  negbii 187  mpbir 190  sylibr 200  sylbir 201  syl5ibr 207  syl6ibr 213  con1bii 220  pm2.54 227  pm2.68 250  pm2.31 261  pm3.2 283  pm3.11 315  pm3.31 349  pm3.44 430  sylanbr 450  sylan2br 453  anbi2i 480  dfbi 515  pm3.43 603  pm5.15 666  syl3an1br 865  syl3an2br 866  syl3an3br 867  nicodraw 952  mpgbir 988  sbbii 1174  a12lem1 1376  mo2 1400  exmoeu 1413  2euex 1441  2mo 1447  eueq2 1918  eueq3 1919  sspss 2145  neldif 2165  reuss2 2275  pssdifn0 2329  ssunieq 2531  intab 2560  frirr 2924  ordunidif 3005  sucid 3051  unizlim 3113  nnsuc 3148  tfinds 3161  opres 3375  ndmima 3434  fnf 3628  dffo2 3675  f1o2 3693  f1o00 3714  fvimacnvALT 3809  exfo 3822  fopabco 3832  tz7.44-3 3930  tz7.49 3959  abianfp 3962  f1stres 4093  f2ndres 4094  unblem4 4538  inf3lem3 4607  trcl 4637  kmlem1 4757  brdom3 4793  brdom5 4794  brdom4 4795  brdom6disj 4797  ondomcard 4849  ltexpq 5072  suppsr3 5216  axcnre 5278  le2tri3 5581  0nn0 6101  elnnnn0b 6161  elnnnn0c 6162  uzind4 6436  sqr2irrlem1 6710  absdivz 6844  abs1m 6889  seq1ub 6897  binomlem5 7055  iserzex 7131  ivthlem2 7267  ivthlem7 7272  ivthlem8 7273  eff2 7355  ef01tlub 7371  absef01tlub 7373  efcnlem1 7404  sincos1sgn 7464  sincos2sgn 7465  znnen 7487  tgclt 7609  sn0top 7632  elcls 7689  cnpfval 7742  cnconst 7765  blval 7822  bl2in 7828  bcthlem17 8000  grplactf1o 8083  issubgi 8107  subgabl 8108  ghgrpi 8122  sm1cnilem 8332  blo3i 8447  pilem1 8656  pilem3 8658  sinhalfpilem 8664  sincos4thpi 8695  sincos6thpi 8696  cosh111t 8702  efif 8706  efifolem1 8707  efifolem2 8708  efifolem3 8709  efifolem5 8711  efifolem6 8712  efif1lem6 8720  efielcirc 8724  effoi 8730  resslogrn 8738  pilog 8753  hhsscms 9135  hsupval2t 9285  cmcmlem 9519  lnopcon 9948  lnfncon 9975  cnvbravalt 10028  leopnmidt 10056  csmdsym 10246  irredlem4 10305  sumdmdlem 10330  ghomfo 10376  ghomf1olem 10381  fiv 10459  oefil2 10526  filintf 10528  fisubNEW 10532  fisub 10533  isalg 10596

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

Copyright terms: Public domain