Theorem biimpri 133

Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)

Hypothesis

Ref	Expression
biimpri.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biimpri	⊢ (𝜓 → 𝜑)

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	bicomi 132	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 120	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylibr  134  sylbir  135  sylbbr  136  sylbb1  137  sylbb2  138  mpbir  146  biimtrrid  153  imbitrrdi  162  bitri  184  sylanbr  285  sylan2br  288  simplbi2  385  sylanblrc  416  mtbi  674  pm3.44  720  orbi2i  767  pm2.31  773  dcor  941  rnlem  982  syl3an1br  1310  syl3an2br  1311  syl3an3br  1312  xorbin  1426  3impexpbicom  1481  equveli  1805  sbbii  1811  dveeq2or  1862  exmoeudc  2141  nfabdw  2391  eueq2dc  2977  ralun  3387  undif3ss  3466  ssunieq  3924  a9evsep  4209  dcextest  4677  tfi  4678  peano5  4694  opelxpi  4755  ndmima  5111  iotass  5302  dffo2  5560  dff1o2  5585  resdif  5602  f1o00  5616  ressnop0  5830  fsnunfv  5850  ovid  6133  ovidig  6134  f1stres  6317  f2ndres  6318  rdgon  6547  elixpsn  6899  modom  6989  diffisn  7075  diffifi  7076  unsnfi  7104  snexxph  7140  ordiso2  7225  omp1eomlem  7284  ltexnqq  7618  enq0sym  7642  prarloclem5  7710  nqprloc  7755  nqprl  7761  nqpru  7762  pitonn  8058  axcnre  8091  peano5nnnn  8102  axcaucvglemres  8109  le2tri3i  8278  muldivdirap  8877  peano5nni  9136  0nn0  9407  uzind4  9812  elfz4  10243  eluzfz  10245  ssfzo12bi  10460  ioom  10510  ser0  10785  exp3vallem  10792  hashinfuni  11029  hashxp  11080  wrdsymb1  11140  ccatfv0  11170  lswccats1fst  11211  ccatswrd  11241  ccatpfx  11272  nn0abscl  11636  fimaxre2  11778  iserle  11893  climserle  11896  summodclem2a  11932  fsumcl2lem  11949  fsumadd  11957  sumsnf  11960  isumclim3  11974  isumadd  11982  sumsplitdc  11983  fsummulc2  11999  cvgcmpub  12027  isumshft  12041  isumlessdc  12047  trireciplem  12051  geolim  12062  geo2lim  12067  cvgratz  12083  mertenslem2  12087  mertensabs  12088  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodmul  12142  prodsnf  12143  ef0lem  12211  efcvgfsum  12218  ege2le3  12222  efcj  12224  efgt1p2  12246  ndvdsadd  12482  gcdsupex  12518  gcdsupcl  12519  ialgrlemconst  12605  divgcdcoprmex  12664  1idssfct  12677  odzdvds  12808  nninfdclemp1  13061  divsfval  13401  xpsfrnel2  13419  xpsff1o  13422  mulgnndir  13728  rmodislmodlem  14354  rmodislmod  14355  tgcl  14778  txcnp  14985  ivthdich  15367  plyval  15446  lgsval2lem  15729  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsmodeq  15764  lgsmulsqcoprm  15765  2lgs  15823  bj-charfunbi  16342  bj-sucexg  16453  bj-indind  16463  bj-2inf  16469  findset  16476  trilpolemisumle  16578  nconstwlpolem0  16603