Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpri 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  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
 Copyright terms: Public domain W3C validator