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  pm3.43 602  pm5.15 665  syl3an1br 864  syl3an2br 865  syl3an3br 866  nicodraw 950  mpgbir 986  sbbii 1172  a12lem1 1374  mo2 1398  exmoeu 1411  2euex 1439  2mo 1445  eueq2 1914  eueq3 1915  sspss 2141  neldif 2161  reuss2 2271  pssdifn0 2325  ssunieq 2526  intab 2555  frirr 2919  ordunidif 3000  sucid 3046  unizlim 3108  nnsuc 3143  tfinds 3156  opres 3367  ndmima 3426  fnf 3620  dffo2 3666  f1o2 3684  f1o00 3705  fvimacnvALT 3800  exfo 3813  fopabco 3823  tz7.44-3 3921  tz7.49 3950  abianfp 3953  f1stres 4083  f2ndres 4084  unblem4 4526  inf3lem3 4595  trcl 4625  kmlem1 4745  brdom3 4781  brdom5 4782  brdom4 4783  brdom6disj 4785  ondomcard 4837  ltexpq 5060  suppsr3 5204  axcnre 5266  le2tri3 5571  0nn0 6068  elnnnn0b 6128  elnnnn0c 6129  uzind4 6390  sqr2irrlem1 6662  absdivz 6802  abs1m 6849  seq1ub 6857  binomlem5 7016  iserzex 7090  ivthlem2 7225  ivthlem7 7230  ivthlem8 7231  ivthlem7OLD 7239  ivthlem8OLD 7240  ivth2OLD 7242  eff2 7320  ef01tlub 7335  absef01tlub 7337  efcnlem1 7367  sincos1sgn 7429  sincos2sgn 7430  znnen 7453  tgclt 7574  sn0top 7597  elcls 7654  cnpfval 7707  cnconst 7730  blval 7789  bl2in 7795  bcthlem17 7965  grplactf1o 8049  issubgi 8074  subgabl 8075  ghgrpi 8089  sm1cnilem 8294  blo3i 8406  pilem1 8609  pilem3 8611  sinhalfpilem 8617  sincos4thpi 8646  sincos6thpi 8647  cosh111t 8651  efif 8655  efifolem1 8656  efifolem2 8657  efifolem3 8658  efifolem5 8660  efifolem6 8661  efif1lem6 8669  efielcircOLD 8674  circgrpOLD 8677  efielcirc 8678  effoi 8684  resslogrn 8692  pilog 8707  hhsscms 9089  hsupval2t 9238  cmcmlem 9474  lnopcon 9901  lnfncon 9928  cnvbravalt 9981  leopnmidt 10009  csmdsym 10198  irredlem4 10257  sumdmdlem 10281  ghomfo 10325  ghomf1olem 10330  fiv 10410  oefil2 10477  filintf 10479  fisub 10483  isalg 10533

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