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 ⊢ (𝜓 → 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3968  a9evsep  4257  uniex2  4583  dcextest  4730  tfi  4731  peano5  4747  opelxpi  4808  ndmima  5167  iotass  5358  dffo2  5622  dff1o2  5647  resdif  5664  f1o00  5679  ressnop0  5899  fsnunfv  5919  ovid  6208  ovidig  6209  f1stres  6397  f2ndres  6398  rdgon  6662  elixpsn  7023  modom  7114  diffisn  7203  diffifi  7204  unsnfi  7232  snexxph  7274  ordiso2  7381  omp1eomlem  7440  ltexnqq  7781  enq0sym  7805  prarloclem5  7873  nqprloc  7918  nqprl  7924  nqpru  7925  pitonn  8221  axcnre  8254  peano5nnnn  8265  axcaucvglemres  8272  le2tri3i  8441  muldivdirap  9045  peano5nni  9316  0nn0  9589  uzind4  10003  elfz4  10437  eluzfz  10439  ssfzo12bi  10659  ioom  10711  ser0  10990  exp3vallem  10997  hashinfuni  11237  hashxp  11288  wrdsymb1  11362  ccatfv0  11392  lswccats1fst  11433  ccatswrd  11463  ccatpfx  11494  nn0abscl  11873  fimaxre2  12015  iserle  12132  climserle  12135  summodclem2a  12172  fsumcl2lem  12189  fsumadd  12197  sumsnf  12200  isumclim3  12214  isumadd  12222  sumsplitdc  12223  fsummulc2  12239  cvgcmpub  12267  isumshft  12281  isumlessdc  12287  trireciplem  12291  geolim  12302  geo2lim  12307  cvgratz  12323  mertenslem2  12327  mertensabs  12328  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodmul  12382  prodsnf  12383  ef0lem  12451  efcvgfsum  12458  ege2le3  12462  efcj  12464  efgt1p2  12486  ndvdsadd  12722  gcdsupex  12758  gcdsupcl  12759  ialgrlemconst  12845  divgcdcoprmex  12904  1idssfct  12917  odzdvds  13052  nninfdclemp1  13398  divsfval  13707  xpsfrnel2  13725  xpsff1o  13728  mulgnndir  14012  gsummptfidmsplit  14253  gsumresfi  14262  opprdrng  14728  rmodislmodlem  14795  rmodislmod  14796  isassa  15110  tgcl  15307  txcnp  15514  ivthdich  15896  plyval  15975  logfac  16143  lgsval2lem  16351  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsmodeq  16386  lgsmulsqcoprm  16387  2lgs  16445  bj-charfunbi  17059  bj-sucexg  17170  bj-indind  17180  bj-2inf  17186  findset  17193  trilpolemisumle  17311  nconstwlpolem0  17337