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  4255  uniex2  4581  dcextest  4728  tfi  4729  peano5  4745  opelxpi  4806  ndmima  5164  iotass  5355  dffo2  5619  dff1o2  5644  resdif  5661  f1o00  5676  ressnop0  5896  fsnunfv  5916  ovid  6205  ovidig  6206  f1stres  6393  f2ndres  6394  rdgon  6657  elixpsn  7017  modom  7108  diffisn  7197  diffifi  7198  unsnfi  7226  snexxph  7267  ordiso2  7376  omp1eomlem  7435  ltexnqq  7776  enq0sym  7800  prarloclem5  7868  nqprloc  7913  nqprl  7919  nqpru  7920  pitonn  8216  axcnre  8249  peano5nnnn  8260  axcaucvglemres  8267  le2tri3i  8436  muldivdirap  9040  peano5nni  9310  0nn0  9583  uzind4  9998  elfz4  10432  eluzfz  10434  ssfzo12bi  10654  ioom  10706  ser0  10984  exp3vallem  10991  hashinfuni  11231  hashxp  11282  wrdsymb1  11356  ccatfv0  11386  lswccats1fst  11427  ccatswrd  11457  ccatpfx  11488  nn0abscl  11867  fimaxre2  12009  iserle  12126  climserle  12129  summodclem2a  12166  fsumcl2lem  12183  fsumadd  12191  sumsnf  12194  isumclim3  12208  isumadd  12216  sumsplitdc  12217  fsummulc2  12233  cvgcmpub  12261  isumshft  12275  isumlessdc  12281  trireciplem  12285  geolim  12296  geo2lim  12301  cvgratz  12317  mertenslem2  12321  mertensabs  12322  prodmodclem3  12360  prodmodclem2a  12361  zproddc  12364  fprodmul  12376  prodsnf  12377  ef0lem  12445  efcvgfsum  12452  ege2le3  12456  efcj  12458  efgt1p2  12480  ndvdsadd  12716  gcdsupex  12752  gcdsupcl  12753  ialgrlemconst  12839  divgcdcoprmex  12898  1idssfct  12911  odzdvds  13046  nninfdclemp1  13392  divsfval  13700  xpsfrnel2  13718  xpsff1o  13721  mulgnndir  14005  opprdrng  14671  rmodislmodlem  14738  rmodislmod  14739  isassa  15053  tgcl  15217  txcnp  15424  ivthdich  15806  plyval  15885  logfac  16051  lgsval2lem  16251  lgsdir  16276  lgsdilem2  16277  lgsdi  16278  lgsne0  16279  lgsmodeq  16286  lgsmulsqcoprm  16287  2lgs  16345  bj-charfunbi  16959  bj-sucexg  17070  bj-indind  17080  bj-2inf  17086  findset  17093  trilpolemisumle  17209  nconstwlpolem0  17235