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  biranri  388  bilanri  389  sylanblrc  420  mtbi  681  pm3.44  727  orbi2i  774  pm2.31  780  dcor  948  rnlem  989  syl3an1br  1317  syl3an2br  1318  syl3an3br  1319  xorbin  1433  3impexpbicom  1488  equveli  1812  sbbii  1818  dveeq2or  1869  exmoeudc  2150  nfabdw  2411  eueq2dc  2999  ralun  3411  undif3ss  3492  ssunieq  3963  a9evsep  4250  uniex2  4576  dcextest  4723  tfi  4724  peano5  4740  opelxpi  4801  ndmima  5159  iotass  5350  dffo2  5614  dff1o2  5639  resdif  5656  f1o00  5671  ressnop0  5887  fsnunfv  5907  ovid  6195  ovidig  6196  f1stres  6383  f2ndres  6384  rdgon  6647  elixpsn  7007  modom  7098  diffisn  7187  diffifi  7188  unsnfi  7216  snexxph  7257  ordiso2  7365  omp1eomlem  7424  ltexnqq  7765  enq0sym  7789  prarloclem5  7857  nqprloc  7902  nqprl  7908  nqpru  7909  pitonn  8205  axcnre  8238  peano5nnnn  8249  axcaucvglemres  8256  le2tri3i  8424  muldivdirap  9027  peano5nni  9286  0nn0  9557  uzind4  9967  elfz4  10400  eluzfz  10402  ssfzo12bi  10621  ioom  10673  ser0  10948  exp3vallem  10955  hashinfuni  11194  hashxp  11245  wrdsymb1  11319  ccatfv0  11349  lswccats1fst  11390  ccatswrd  11420  ccatpfx  11451  nn0abscl  11829  fimaxre2  11971  iserle  12086  climserle  12089  summodclem2a  12126  fsumcl2lem  12143  fsumadd  12151  sumsnf  12154  isumclim3  12168  isumadd  12176  sumsplitdc  12177  fsummulc2  12193  cvgcmpub  12221  isumshft  12235  isumlessdc  12241  trireciplem  12245  geolim  12256  geo2lim  12261  cvgratz  12277  mertenslem2  12281  mertensabs  12282  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodmul  12336  prodsnf  12337  ef0lem  12405  efcvgfsum  12412  ege2le3  12416  efcj  12418  efgt1p2  12440  ndvdsadd  12676  gcdsupex  12712  gcdsupcl  12713  ialgrlemconst  12799  divgcdcoprmex  12858  1idssfct  12871  odzdvds  13002  nninfdclemp1  13319  divsfval  13626  xpsfrnel2  13644  xpsff1o  13647  mulgnndir  13931  opprdrng  14593  rmodislmodlem  14659  rmodislmod  14660  tgcl  15088  txcnp  15295  ivthdich  15677  plyval  15756  logfac  15918  lgsval2lem  16043  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsmodeq  16078  lgsmulsqcoprm  16079  2lgs  16137  bj-charfunbi  16751  bj-sucexg  16862  bj-indind  16872  bj-2inf  16878  findset  16885  trilpolemisumle  16992  nconstwlpolem0  17018