Theorem biimpri 124

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 123	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 113	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sylbir  125  mpbir  134  sylibr  137  syl5bir  142  syl6ibr  151  bitri  173  sylanbr  269  sylan2br  272  simplbi2  367  mtbi  595  pm3.44  635  orbi2i  679  pm2.31  685  dcor  843  rnlem  883  syl3an1br  1174  syl3an2br  1175  syl3an3br  1176  xorbin  1275  3impexpbicom  1327  equveli  1642  sbbii  1648  dveeq2or  1697  exmoeudc  1963  eueq2dc  2714  ralun  3125  undif3ss  3198  ssunieq  3613  a9evsep  3879  tfi  4305  peano5  4321  opelxpi  4376  ndmima  4702  iotass  4884  dffo2  5110  dff1o2  5131  resdif  5148  f1o00  5161  ressnop0  5344  fsnunfv  5363  ovid  5617  ovidig  5618  f1stres  5786  f2ndres  5787  diffisn  6350  diffifi  6351  ordiso2  6357  ltexnqq  6506  enq0sym  6530  prarloclem5  6598  nqprloc  6643  nqprl  6649  nqpru  6650  pitonn  6924  axcnre  6955  peano5nnnn  6966  axcaucvglemres  6973  le2tri3i  7126  peano5nni  7917  0nn0  8196  uzind4  8531  elfz4  8883  eluzfz  8885  ssfzo12bi  9081  iser0  9250  nn0abscl  9681  iserile  9862  ialgrlemconst  9882  bj-sucexg  10042  bj-indind  10056  bj-2inf  10062  peano5setOLD  10065  findset  10070