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  677  pm3.44  723  orbi2i  770  pm2.31  776  dcor  944  rnlem  985  syl3an1br  1313  syl3an2br  1314  syl3an3br  1315  xorbin  1429  3impexpbicom  1484  equveli  1807  sbbii  1813  dveeq2or  1864  exmoeudc  2143  nfabdw  2394  eueq2dc  2980  ralun  3391  undif3ss  3470  ssunieq  3931  a9evsep  4216  dcextest  4685  tfi  4686  peano5  4702  opelxpi  4763  ndmima  5120  iotass  5311  dffo2  5572  dff1o2  5597  resdif  5614  f1o00  5629  ressnop0  5843  fsnunfv  5863  ovid  6148  ovidig  6149  f1stres  6331  f2ndres  6332  rdgon  6595  elixpsn  6947  modom  7037  diffisn  7125  diffifi  7126  unsnfi  7154  snexxph  7192  ordiso2  7277  omp1eomlem  7336  ltexnqq  7671  enq0sym  7695  prarloclem5  7763  nqprloc  7808  nqprl  7814  nqpru  7815  pitonn  8111  axcnre  8144  peano5nnnn  8155  axcaucvglemres  8162  le2tri3i  8330  muldivdirap  8929  peano5nni  9188  0nn0  9459  uzind4  9866  elfz4  10298  eluzfz  10300  ssfzo12bi  10516  ioom  10566  ser0  10841  exp3vallem  10848  hashinfuni  11085  hashxp  11136  wrdsymb1  11199  ccatfv0  11229  lswccats1fst  11270  ccatswrd  11300  ccatpfx  11331  nn0abscl  11708  fimaxre2  11850  iserle  11965  climserle  11968  summodclem2a  12005  fsumcl2lem  12022  fsumadd  12030  sumsnf  12033  isumclim3  12047  isumadd  12055  sumsplitdc  12056  fsummulc2  12072  cvgcmpub  12100  isumshft  12114  isumlessdc  12120  trireciplem  12124  geolim  12135  geo2lim  12140  cvgratz  12156  mertenslem2  12160  mertensabs  12161  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodmul  12215  prodsnf  12216  ef0lem  12284  efcvgfsum  12291  ege2le3  12295  efcj  12297  efgt1p2  12319  ndvdsadd  12555  gcdsupex  12591  gcdsupcl  12592  ialgrlemconst  12678  divgcdcoprmex  12737  1idssfct  12750  odzdvds  12881  nninfdclemp1  13134  divsfval  13474  xpsfrnel2  13492  xpsff1o  13495  mulgnndir  13801  rmodislmodlem  14429  rmodislmod  14430  tgcl  14858  txcnp  15065  ivthdich  15447  plyval  15526  lgsval2lem  15812  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgsmodeq  15847  lgsmulsqcoprm  15848  2lgs  15906  bj-charfunbi  16510  bj-sucexg  16621  bj-indind  16631  bj-2inf  16637  findset  16644  trilpolemisumle  16753  nconstwlpolem0  16779