ILE Home 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  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpri  |-  ( ps 
->  ph )

Proof of Theorem biimpri
StepHypRef Expression
1 biimpri.1 . . 3  |-  ( ph  <->  ps )
21bicomi 123 . 2  |-  ( ps  <->  ph )
32biimpi 113 1  |-  ( ps 
->  ph )
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  6355  ltexnqq  6504  enq0sym  6528  prarloclem5  6596  nqprloc  6641  nqprl  6647  nqpru  6648  pitonn  6922  axcnre  6953  peano5nnnn  6964  axcaucvglemres  6971  le2tri3i  7124  peano5nni  7915  0nn0  8194  uzind4  8529  elfz4  8881  eluzfz  8883  ssfzo12bi  9079  iser0  9224  nn0abscl  9655  iserile  9836  ialgrlemconst  9856  bj-sucexg  10016  bj-indind  10030  bj-2inf  10036  peano5setOLD  10039  findset  10044
  Copyright terms: Public domain W3C validator