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

Theorem biimpri 132
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 131 . 2 (𝜓𝜑)
32biimpi 119 1 (𝜓𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylibr  133  sylbir  134  sylbbr  135  sylbb1  136  sylbb2  137  mpbir  145  syl5bir  152  syl6ibr  161  bitri  183  sylanbr  283  sylan2br  286  simplbi2  382  sylanblrc  412  mtbi  659  pm3.44  704  orbi2i  751  pm2.31  757  dcor  919  rnlem  960  syl3an1br  1255  syl3an2br  1256  syl3an3br  1257  xorbin  1362  3impexpbicom  1414  equveli  1732  sbbii  1738  dveeq2or  1788  exmoeudc  2062  eueq2dc  2857  ralun  3258  undif3ss  3337  ssunieq  3769  a9evsep  4050  dcextest  4495  tfi  4496  peano5  4512  opelxpi  4571  ndmima  4916  iotass  5105  dffo2  5349  dff1o2  5372  resdif  5389  f1o00  5402  ressnop0  5601  fsnunfv  5621  ovid  5887  ovidig  5888  f1stres  6057  f2ndres  6058  rdgon  6283  elixpsn  6629  diffisn  6787  diffifi  6788  unsnfi  6807  snexxph  6838  ordiso2  6920  omp1eomlem  6979  ltexnqq  7228  enq0sym  7252  prarloclem5  7320  nqprloc  7365  nqprl  7371  nqpru  7372  pitonn  7668  axcnre  7701  peano5nnnn  7712  axcaucvglemres  7719  le2tri3i  7884  muldivdirap  8479  peano5nni  8735  0nn0  9004  uzind4  9395  elfz4  9811  eluzfz  9813  ssfzo12bi  10014  ioom  10050  ser0  10299  exp3vallem  10306  hashinfuni  10535  hashxp  10584  nn0abscl  10869  fimaxre2  11010  iserle  11123  climserle  11126  summodclem2a  11162  fsumcl2lem  11179  fsumadd  11187  sumsnf  11190  isumclim3  11204  isumadd  11212  sumsplitdc  11213  fsummulc2  11229  cvgcmpub  11257  isumshft  11271  isumlessdc  11277  trireciplem  11281  geolim  11292  geo2lim  11297  cvgratz  11313  mertenslem2  11317  mertensabs  11318  prodmodclem3  11356  prodmodclem2a  11357  ef0lem  11378  efcvgfsum  11385  ege2le3  11389  efcj  11391  efgt1p2  11413  ndvdsadd  11639  gcdsupex  11657  gcdsupcl  11658  ialgrlemconst  11735  divgcdcoprmex  11794  1idssfct  11807  tgcl  12247  txcnp  12454  bj-sucexg  13179  bj-indind  13189  bj-2inf  13195  findset  13202  trilpolemisumle  13292
  Copyright terms: Public domain W3C validator