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  2976  ralun  3386  undif3ss  3465  ssunieq  3920  a9evsep  4205  dcextest  4672  tfi  4673  peano5  4689  opelxpi  4750  ndmima  5104  iotass  5295  dffo2  5551  dff1o2  5576  resdif  5593  f1o00  5607  ressnop0  5819  fsnunfv  5839  ovid  6120  ovidig  6121  f1stres  6303  f2ndres  6304  rdgon  6530  elixpsn  6880  diffisn  7051  diffifi  7052  unsnfi  7077  snexxph  7113  ordiso2  7198  omp1eomlem  7257  ltexnqq  7591  enq0sym  7615  prarloclem5  7683  nqprloc  7728  nqprl  7734  nqpru  7735  pitonn  8031  axcnre  8064  peano5nnnn  8075  axcaucvglemres  8082  le2tri3i  8251  muldivdirap  8850  peano5nni  9109  0nn0  9380  uzind4  9779  elfz4  10210  eluzfz  10212  ssfzo12bi  10426  ioom  10475  ser0  10750  exp3vallem  10757  hashinfuni  10994  hashxp  11043  wrdsymb1  11103  ccatfv0  11133  lswccats1fst  11170  ccatswrd  11197  ccatpfx  11228  nn0abscl  11591  fimaxre2  11733  iserle  11848  climserle  11851  summodclem2a  11887  fsumcl2lem  11904  fsumadd  11912  sumsnf  11915  isumclim3  11929  isumadd  11937  sumsplitdc  11938  fsummulc2  11954  cvgcmpub  11982  isumshft  11996  isumlessdc  12002  trireciplem  12006  geolim  12017  geo2lim  12022  cvgratz  12038  mertenslem2  12042  mertensabs  12043  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodmul  12097  prodsnf  12098  ef0lem  12166  efcvgfsum  12173  ege2le3  12177  efcj  12179  efgt1p2  12201  ndvdsadd  12437  gcdsupex  12473  gcdsupcl  12474  ialgrlemconst  12560  divgcdcoprmex  12619  1idssfct  12632  odzdvds  12763  nninfdclemp1  13016  divsfval  13356  xpsfrnel2  13374  xpsff1o  13377  mulgnndir  13683  rmodislmodlem  14308  rmodislmod  14309  tgcl  14732  txcnp  14939  ivthdich  15321  plyval  15400  lgsval2lem  15683  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  lgsmodeq  15718  lgsmulsqcoprm  15719  2lgs  15777  bj-charfunbi  16132  bj-sucexg  16243  bj-indind  16253  bj-2inf  16259  findset  16266  trilpolemisumle  16365  nconstwlpolem0  16390