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  676  pm3.44  722  orbi2i  769  pm2.31  775  dcor  943  rnlem  984  syl3an1br  1312  syl3an2br  1313  syl3an3br  1314  xorbin  1428  3impexpbicom  1483  equveli  1807  sbbii  1813  dveeq2or  1864  exmoeudc  2143  nfabdw  2393  eueq2dc  2979  ralun  3389  undif3ss  3468  ssunieq  3926  a9evsep  4211  dcextest  4679  tfi  4680  peano5  4696  opelxpi  4757  ndmima  5113  iotass  5304  dffo2  5563  dff1o2  5588  resdif  5605  f1o00  5620  ressnop0  5835  fsnunfv  5855  ovid  6138  ovidig  6139  f1stres  6322  f2ndres  6323  rdgon  6552  elixpsn  6904  modom  6994  diffisn  7082  diffifi  7083  unsnfi  7111  snexxph  7149  ordiso2  7234  omp1eomlem  7293  ltexnqq  7628  enq0sym  7652  prarloclem5  7720  nqprloc  7765  nqprl  7771  nqpru  7772  pitonn  8068  axcnre  8101  peano5nnnn  8112  axcaucvglemres  8119  le2tri3i  8288  muldivdirap  8887  peano5nni  9146  0nn0  9417  uzind4  9822  elfz4  10253  eluzfz  10255  ssfzo12bi  10471  ioom  10521  ser0  10796  exp3vallem  10803  hashinfuni  11040  hashxp  11091  wrdsymb1  11154  ccatfv0  11184  lswccats1fst  11225  ccatswrd  11255  ccatpfx  11286  nn0abscl  11650  fimaxre2  11792  iserle  11907  climserle  11910  summodclem2a  11947  fsumcl2lem  11964  fsumadd  11972  sumsnf  11975  isumclim3  11989  isumadd  11997  sumsplitdc  11998  fsummulc2  12014  cvgcmpub  12042  isumshft  12056  isumlessdc  12062  trireciplem  12066  geolim  12077  geo2lim  12082  cvgratz  12098  mertenslem2  12102  mertensabs  12103  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodmul  12157  prodsnf  12158  ef0lem  12226  efcvgfsum  12233  ege2le3  12237  efcj  12239  efgt1p2  12261  ndvdsadd  12497  gcdsupex  12533  gcdsupcl  12534  ialgrlemconst  12620  divgcdcoprmex  12679  1idssfct  12692  odzdvds  12823  nninfdclemp1  13076  divsfval  13416  xpsfrnel2  13434  xpsff1o  13437  mulgnndir  13743  rmodislmodlem  14370  rmodislmod  14371  tgcl  14794  txcnp  15001  ivthdich  15383  plyval  15462  lgsval2lem  15745  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsmodeq  15780  lgsmulsqcoprm  15781  2lgs  15839  bj-charfunbi  16432  bj-sucexg  16543  bj-indind  16553  bj-2inf  16559  findset  16566  trilpolemisumle  16668  nconstwlpolem0  16694