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  671  pm3.44  716  orbi2i  763  pm2.31  769  dcor  937  rnlem  978  syl3an1br  1288  syl3an2br  1289  syl3an3br  1290  xorbin  1395  3impexpbicom  1449  equveli  1773  sbbii  1779  dveeq2or  1830  exmoeudc  2108  nfabdw  2358  eueq2dc  2937  ralun  3345  undif3ss  3424  ssunieq  3872  a9evsep  4155  dcextest  4617  tfi  4618  peano5  4634  opelxpi  4695  ndmima  5046  iotass  5236  dffo2  5484  dff1o2  5509  resdif  5526  f1o00  5539  ressnop0  5743  fsnunfv  5763  ovid  6039  ovidig  6040  f1stres  6217  f2ndres  6218  rdgon  6444  elixpsn  6794  diffisn  6954  diffifi  6955  unsnfi  6980  snexxph  7016  ordiso2  7101  omp1eomlem  7160  ltexnqq  7475  enq0sym  7499  prarloclem5  7567  nqprloc  7612  nqprl  7618  nqpru  7619  pitonn  7915  axcnre  7948  peano5nnnn  7959  axcaucvglemres  7966  le2tri3i  8135  muldivdirap  8734  peano5nni  8993  0nn0  9264  uzind4  9662  elfz4  10093  eluzfz  10095  ssfzo12bi  10301  ioom  10350  ser0  10625  exp3vallem  10632  hashinfuni  10869  hashxp  10918  wrdsymb1  10971  nn0abscl  11250  fimaxre2  11392  iserle  11507  climserle  11510  summodclem2a  11546  fsumcl2lem  11563  fsumadd  11571  sumsnf  11574  isumclim3  11588  isumadd  11596  sumsplitdc  11597  fsummulc2  11613  cvgcmpub  11641  isumshft  11655  isumlessdc  11661  trireciplem  11665  geolim  11676  geo2lim  11681  cvgratz  11697  mertenslem2  11701  mertensabs  11702  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodmul  11756  prodsnf  11757  ef0lem  11825  efcvgfsum  11832  ege2le3  11836  efcj  11838  efgt1p2  11860  ndvdsadd  12096  gcdsupex  12124  gcdsupcl  12125  ialgrlemconst  12211  divgcdcoprmex  12270  1idssfct  12283  odzdvds  12414  nninfdclemp1  12667  divsfval  12971  xpsfrnel2  12989  xpsff1o  12992  mulgnndir  13281  rmodislmodlem  13906  rmodislmod  13907  tgcl  14300  txcnp  14507  ivthdich  14889  plyval  14968  lgsval2lem  15251  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsmodeq  15286  lgsmulsqcoprm  15287  2lgs  15345  bj-charfunbi  15457  bj-sucexg  15568  bj-indind  15578  bj-2inf  15584  findset  15591  trilpolemisumle  15682  nconstwlpolem0  15707