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  5834  fsnunfv  5854  ovid  6137  ovidig  6138  f1stres  6321  f2ndres  6322  rdgon  6551  elixpsn  6903  modom  6993  diffisn  7081  diffifi  7082  unsnfi  7110  snexxph  7148  ordiso2  7233  omp1eomlem  7292  ltexnqq  7627  enq0sym  7651  prarloclem5  7719  nqprloc  7764  nqprl  7770  nqpru  7771  pitonn  8067  axcnre  8100  peano5nnnn  8111  axcaucvglemres  8118  le2tri3i  8287  muldivdirap  8886  peano5nni  9145  0nn0  9416  uzind4  9821  elfz4  10252  eluzfz  10254  ssfzo12bi  10469  ioom  10519  ser0  10794  exp3vallem  10801  hashinfuni  11038  hashxp  11089  wrdsymb1  11149  ccatfv0  11179  lswccats1fst  11220  ccatswrd  11250  ccatpfx  11281  nn0abscl  11645  fimaxre2  11787  iserle  11902  climserle  11905  summodclem2a  11941  fsumcl2lem  11958  fsumadd  11966  sumsnf  11969  isumclim3  11983  isumadd  11991  sumsplitdc  11992  fsummulc2  12008  cvgcmpub  12036  isumshft  12050  isumlessdc  12056  trireciplem  12060  geolim  12071  geo2lim  12076  cvgratz  12092  mertenslem2  12096  mertensabs  12097  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodmul  12151  prodsnf  12152  ef0lem  12220  efcvgfsum  12227  ege2le3  12231  efcj  12233  efgt1p2  12255  ndvdsadd  12491  gcdsupex  12527  gcdsupcl  12528  ialgrlemconst  12614  divgcdcoprmex  12673  1idssfct  12686  odzdvds  12817  nninfdclemp1  13070  divsfval  13410  xpsfrnel2  13428  xpsff1o  13431  mulgnndir  13737  rmodislmodlem  14363  rmodislmod  14364  tgcl  14787  txcnp  14994  ivthdich  15376  plyval  15455  lgsval2lem  15738  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsmodeq  15773  lgsmulsqcoprm  15774  2lgs  15832  bj-charfunbi  16406  bj-sucexg  16517  bj-indind  16527  bj-2inf  16533  findset  16540  trilpolemisumle  16642  nconstwlpolem0  16667