ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  impbid2 GIF 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 (𝜓𝜒)
impbid2.2 (𝜑 → (𝜒𝜓))
Assertion
Ref Expression
impbid2 (𝜑 → (𝜓𝜒))

Proof of Theorem impbid2
StepHypRef Expression
1 impbid2.2 . . 3 (𝜑 → (𝜒𝜓))
2 impbid2.1 . . 3 (𝜓𝜒)
31, 2impbid1 141 . 2 (𝜑 → (𝜒𝜓))
43bicomd 140 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:  biimt  240  mtt  674  biorf  733  biorfi  735  pm4.72  812  biort  814  con34bdc  856  notnotbdc  857  dfandc  869  imanst  873  dfordc  877  dfor2dc  880  pm4.79dc  888  orimdidc  891  pm5.54dc  903  pm5.62dc  929  bimsc1  947  modc  2040  euan  2053  exmoeudc  2060  nebidc  2386  cgsexg  2716  cgsex2g  2717  cgsex4g  2718  elab3gf  2829  abidnf  2847  elsn2g  3553  difsn  3652  prel12  3693  dfnfc2  3749  intmin4  3794  dfiin2g  3841  elpw2g  4076  ordsucg  4413  ssrel  4622  ssrel2  4624  ssrelrel  4634  releldmb  4771  relelrnb  4772  cnveqb  4989  dmsnopg  5005  relcnvtr  5053  relcnvexb  5073  f1ocnvb  5374  ffvresb  5576  fconstfvm  5631  fnoprabg  5865  dfsmo2  6177  nntri2  6383  nntri1  6385  en1bg  6687  fieq0  6857  djulclb  6933  ismkvnex  7022  nngt1ne1  8748  znegclb  9080  iccneg  9765  fzsn  9839  fz1sbc  9869  fzofzp1b  9998  ceilqidz  10082  flqeqceilz  10084  reim0b  10627  rexanre  10985  dvdsext  11542  zob  11577  eltg3  12215  bastop  12233  cnptoprest  12397  bj-om  13124
  Copyright terms: Public domain W3C validator