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

Theorem impbid2 142
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 141 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 140 1  |-  ( ph  ->  ( ps  <->  ch )
)
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:  biimt  240  mtt  675  biorf  734  biorfi  736  pm4.72  813  biort  815  con34bdc  857  notnotbdc  858  dfandc  870  imanst  874  dfordc  878  dfor2dc  881  pm4.79dc  889  orimdidc  892  pm5.54dc  904  pm5.62dc  930  bimsc1  948  modc  2043  euan  2056  exmoeudc  2063  nebidc  2389  cgsexg  2722  cgsex2g  2723  cgsex4g  2724  elab3gf  2835  abidnf  2853  elsn2g  3561  difsn  3661  prel12  3702  dfnfc2  3758  intmin4  3803  dfiin2g  3850  elpw2g  4085  ordsucg  4422  ssrel  4631  ssrel2  4633  ssrelrel  4643  releldmb  4780  relelrnb  4781  cnveqb  4998  dmsnopg  5014  relcnvtr  5062  relcnvexb  5082  f1ocnvb  5385  ffvresb  5587  fconstfvm  5642  fnoprabg  5876  dfsmo2  6188  nntri2  6394  nntri1  6396  en1bg  6698  fieq0  6868  djulclb  6944  ismkvnex  7033  nngt1ne1  8775  znegclb  9107  iccneg  9798  fzsn  9873  fz1sbc  9903  fzofzp1b  10032  ceilqidz  10116  flqeqceilz  10118  reim0b  10662  rexanre  11020  dvdsext  11580  zob  11615  eltg3  12256  bastop  12274  cnptoprest  12438  cos11  12973  bj-om  13289
  Copyright terms: Public domain W3C validator