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 479  pm3.43 601  pm5.15 664  syl3an1br 863  syl3an2br 864  syl3an3br 865  nicodraw 949  mpgbir 985  sbbii 1170  a12lem1 1369  mo2 1393  exmoeu 1406  2euex 1434  2mo 1440  eueq2 1909  eueq3 1910  sspss 2135  neldif 2155  reuss2 2265  pssdifn0 2319  ssunieq 2521  intab 2550  frirr 2914  ordunidif 2995  sucid 3041  unizlim 3103  nnsuc 3138  tfinds 3151  opres 3359  ndmima 3418  fnf 3614  dffo2 3660  f1o2 3678  f1o00 3699  fvimacnvALT 3794  exfo 3807  fopabco 3817  tz7.44-3 3915  tz7.49 3944  abianfp 3947  f1stres 4077  f2ndres 4078  unblem4 4520  inf3lem3 4587  trcl 4617  kmlem1 4737  brdom3 4773  brdom5 4774  brdom4 4775  brdom6disj 4777  ondomcard 4829  ltexpq 5052  suppsr3 5196  axcnre 5258  le2tri3 5563  0nn0 6060  elnnnn0b 6120  elnnnn0c 6121  uzind4 6382  sqr2irrlem1 6654  absdivz 6794  abs1m 6841  seq1ub 6849  binomlem5 7008  iserzex 7082  ivthlem2 7217  ivthlem7 7222  ivthlem8 7223  ivthlem7OLD 7231  ivthlem8OLD 7232  ivth2OLD 7234  eff2 7312  ef01tlub 7327  absef01tlub 7329  efcnlem1 7359  sincos1sgn 7421  sincos2sgn 7422  znnen 7445  tgclt 7566  sn0top 7589  elcls 7646  cnpfval 7697  cnconst 7719  blval 7777  bl2in 7783  bcthlem17 7949  grplactf1o 8034  issubgi 8059  subgabl 8060  ghgrpi 8074  sm1cnilem 8281  blo3i 8393  pilem1 8590  pilem3 8592  sinhalfpilem 8598  sincos4thpi 8627  sincos6thpi 8628  cosh111t 8632  efif 8636  efifolem1 8637  efifolem2 8638  efifolem3 8639  efifolem5 8641  efifolem6 8642  efif1lem6 8650  efielcircOLD 8655  circgrpOLD 8658  efielcirc 8659  effoi 8666  effoiOLD 8667  resslogrn 8675  pilog 8690  hhsscms 9067  hsupval2t 9215  cmcmlem 9451  lnopcon 9878  lnfncon 9905  cnvbravalt 9956  leopnmidt 9982  csmdsym 10169  irredlem4 10228  sumdmdlem 10252  ghomfo 10296  ghomf1olem 10301  fiv 10374  oefil2 10441  filintf 10443  fisub 10447  isalg 10497

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