ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpri Structured version   Unicode version

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
StepHypRef Expression
1 biimpri.1 . . 3
21bicomi 123 . 2
32biimpi 113 1
Colors of variables: wff set class
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  594  pm3.44  634  orbi2i  678  pm2.31  684  dcor  842  rnlem  882  syl3an1br  1173  syl3an2br  1174  syl3an3br  1175  xorbin  1272  3impexpbicom  1324  equveli  1639  sbbii  1645  dveeq2or  1694  exmoeudc  1960  eueq2dc  2708  ralun  3119  undif3ss  3192  ssunieq  3604  a9evsep  3870  tfi  4248  peano5  4264  opelxpi  4319  ndmima  4645  iotass  4827  dffo2  5053  dff1o2  5074  resdif  5091  f1o00  5104  ressnop0  5287  fsnunfv  5306  ovid  5559  ovidig  5560  f1stres  5728  f2ndres  5729  ltexnqq  6391  enq0sym  6415  prarloclem5  6483  nqprloc  6528  nqprl  6533  pitonn  6744  axcnre  6765  le2tri3i  6923  peano5nni  7698  0nn0  7972  uzind4  8307  elfz4  8653  eluzfz  8655  ssfzo12bi  8851  nn0abscl  9229  bj-sucexg  9377  bj-indind  9391  bj-2inf  9397  peano5setOLD  9400  findset  9405
  Copyright terms: Public domain W3C validator