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  imanst  777  con34bdc  801  notnotbdc  802  dfandc  814  dfordc  827  dfor2dc  830  pm4.79dc  845  orimdidc  848  pm5.54dc  863  pm5.62dc  889  bimsc1  907  modc  1988  euan  2001  exmoeudc  2008  nebidc  2331  cgsexg  2648  cgsex2g  2649  cgsex4g  2650  elab3gf  2756  abidnf  2774  elsn2g  3462  difsn  3559  prel12  3600  dfnfc2  3656  intmin4  3701  dfiin2g  3748  elpw2g  3969  ordsucg  4294  ssrel  4496  ssrel2  4498  ssrelrel  4508  releldmb  4642  relelrnb  4643  cnveqb  4854  dmsnopg  4870  relcnvtr  4918  relcnvexb  4938  f1ocnvb  5232  ffvresb  5426  fconstfvm  5478  fnoprabg  5705  dfsmo2  6008  nntri2  6211  nntri1  6213  en1bg  6471  djulclb  6694  nngt1ne1  8394  znegclb  8719  iccneg  9341  fzsn  9414  fz1sbc  9443  fzofzp1b  9570  ceilqidz  9654  flqeqceilz  9656  reim0b  10195  rexanre  10552  dvdsext  10762  zob  10797  bj-om  11301
  Copyright terms: Public domain W3C validator