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

Theorem biimpri 128
 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 127 . 2 (𝜓𝜑)
32biimpi 117 1 (𝜓𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  sylbir  129  mpbir  138  sylibr  141  syl5bir  146  syl6ibr  155  bitri  177  sylanbr  273  sylan2br  276  simplbi2  371  sylanblrc  401  mtbi  605  pm3.44  645  orbi2i  689  pm2.31  695  dcor  854  rnlem  894  syl3an1br  1185  syl3an2br  1186  syl3an3br  1187  xorbin  1291  3impexpbicom  1343  equveli  1658  sbbii  1664  dveeq2or  1713  exmoeudc  1979  eueq2dc  2737  ralun  3153  undif3ss  3226  ssunieq  3641  a9evsep  3907  tfi  4333  peano5  4349  opelxpi  4404  ndmima  4730  iotass  4912  dffo2  5138  dff1o2  5159  resdif  5176  f1o00  5189  ressnop0  5372  fsnunfv  5391  ovid  5645  ovidig  5646  f1stres  5814  f2ndres  5815  diffisn  6381  diffifi  6382  ordiso2  6415  ltexnqq  6564  enq0sym  6588  prarloclem5  6656  nqprloc  6701  nqprl  6707  nqpru  6708  pitonn  6982  axcnre  7013  peano5nnnn  7024  axcaucvglemres  7031  le2tri3i  7185  muldivdirap  7758  peano5nni  7993  0nn0  8254  uzind4  8627  elfz4  8985  eluzfz  8987  ssfzo12bi  9183  ioom  9217  iser0  9415  nn0abscl  9912  iserile  10093  ndvdsadd  10243  ialgrlemconst  10265  bj-sucexg  10429  bj-indind  10443  bj-2inf  10449  peano5setOLD  10452  findset  10457
 Copyright terms: Public domain W3C validator