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 4543  inf3lem3 4615  trcl 4645  kmlem1 4765  brdom3 4801  brdom5 4802  brdom4 4803  brdom6disj 4805  ondomcard 4857  ltexpq 5080  suppsr3 5224  axcnre 5286  le2tri3 5589  0nn0 6113  elnnnn0b 6173  elnnnn0c 6174  uzind4 6450  sqr2irrlem1 6724  absdivz 6859  abs1m 6904  seq1ub 6912  binomlem5 7070  iserzex 7146  ivthlem2 7282  ivthlem7 7287  ivthlem8 7288  eff2 7370  ef01tlub 7386  absef01tlub 7388  efcnlem1 7419  sincos1sgn 7479  sincos2sgn 7480  znnen 7502  tgclt 7624  sn0top 7647  elcls 7704  cnpfval 7757  cnconst 7780  blval 7837  bl2in 7843  bcthlem17 8015  grplactf1o 8098  issubgi 8122  subgabl 8123  ghgrpi 8137  sm1cnilem 8347  blo3i 8462  pilem1 8671  pilem3 8673  sinhalfpilem 8679  sincos4thpi 8710  sincos6thpi 8711  cosh111t 8717  efif 8721  efifolem1 8722  efifolem2 8723  efifolem3 8724  efifolem5 8726  efifolem6 8727  efif1lem6 8735  efielcirc 8739  effoi 8745  resslogrn 8753  pilog 8768  hhsscms 9150  hsupval2t 9300  cmcmlem 9534  lnopcon 9963  lnfncon 9990  cnvbravalt 10043  leopnmidt 10071  csmdsym 10261  irredlem4 10320  sumdmdlem 10345  ghomfo 10391  ghomf1olem 10396  fiv 10482  fivOLD 10483  oefil2 10567  filintf 10569  fisub 10576  fisubOLD 10577  isalg 10653

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