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

Theorem impbid2 141
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
Hypotheses
Ref Expression
impbid2.1  |-  ( ps 
->  ch )
impbid2.2  |-  ( ph  ->  ( ch  ->  ps ) )
Assertion
Ref Expression
impbid2  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid2
StepHypRef Expression
1 impbid2.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
2 impbid2.1 . . 3  |-  ( ps 
->  ch )
31, 2impbid1 140 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 139 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimt  239  mtt  643  biorf  696  biorfi  698  pm4.72  770  biort  772  con34bdc  799  notnotbdc  800  dfandc  812  dfordc  825  dfor2dc  828  pm4.79dc  843  orimdidc  846  pm5.54dc  861  pm5.62dc  887  bimsc1  905  modc  1985  euan  1998  exmoeudc  2005  nebidc  2326  cgsexg  2635  cgsex2g  2636  cgsex4g  2637  elab3gf  2744  abidnf  2761  elsn2g  3435  difsn  3531  prel12  3571  dfnfc2  3627  intmin4  3672  dfiin2g  3719  elpw2g  3939  ordsucg  4254  ssrel  4454  ssrel2  4456  ssrelrel  4466  releldmb  4599  relelrnb  4600  cnveqb  4806  dmsnopg  4822  relcnvtr  4870  relcnvexb  4887  f1ocnvb  5171  ffvresb  5360  fconstfvm  5411  fnoprabg  5633  dfsmo2  5936  nntri2  6138  nntri1  6140  en1bg  6347  nngt1ne1  8140  znegclb  8465  iccneg  9087  fzsn  9160  fz1sbc  9189  fzofzp1b  9314  ceilqidz  9398  flqeqceilz  9400  reim0b  9887  rexanre  10244  dvdsext  10400  zob  10435  bj-om  10890
  Copyright terms: Public domain W3C validator