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

Theorem impbid2 135
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 134 . 2 (𝜑 → (𝜒𝜓))
43bicomd 133 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  biimt  234  mtt  620  biorf  673  biorfi  675  pm4.72  747  biort  749  con34bdc  776  notnotbdc  777  dfandc  789  dfordc  802  dfor2dc  805  pm4.79dc  820  orimdidc  823  pm5.54dc  838  pm5.62dc  863  bimsc1  881  modc  1959  euan  1972  exmoeudc  1979  nebidc  2300  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  elab3gf  2715  abidnf  2732  elsn2g  3432  difsn  3529  prel12  3570  dfnfc2  3626  intmin4  3671  dfiin2g  3718  elpw2g  3938  ordsucg  4256  ssrel  4456  ssrel2  4458  ssrelrel  4468  releldmb  4599  relelrnb  4600  cnveqb  4804  dmsnopg  4820  relcnvtr  4868  relcnvexb  4885  f1ocnvb  5168  ffvresb  5356  fconstfvm  5407  fnoprabg  5630  dfsmo2  5933  nntri2  6104  nntri1  6105  en1bg  6311  nngt1ne1  8024  znegclb  8335  iccneg  8958  fzsn  9031  fz1sbc  9060  fzofzp1b  9186  ceilqidz  9266  flqeqceilz  9268  reim0b  9690  dvdsext  10167  zob  10203  bj-om  10448
  Copyright terms: Public domain W3C validator