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

Theorem impbid2 131
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 130 . 2 (φ → (χψ))
43bicomd 129 1 (φ → (ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biimt  230  mtt  609  biorf  662  biorfi  664  pm4.72  735  biort  737  con34bdc  764  notnotdc  765  dfandc  777  dfordc  790  dfor2dc  793  pm4.79dc  808  orimdidc  811  pm5.54dc  826  pm5.62dc  851  bimsc1  869  modc  1940  euan  1953  exmoeudc  1960  nebidc  2279  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  elab3gf  2686  abidnf  2703  elsnc2g  3396  difsn  3492  prel12  3533  dfnfc2  3589  intmin4  3634  dfiin2g  3681  elpw2g  3901  ordsucg  4194  ssrel  4371  ssrel2  4373  ssrelrel  4383  releldmb  4514  relelrnb  4515  cnveqb  4719  dmsnopg  4735  relcnvtr  4783  relcnvexb  4800  f1ocnvb  5083  ffvresb  5271  fconstfvm  5322  fnoprabg  5544  dfsmo2  5843  nntri2  6012  nntri1  6013  en1bg  6216  nngt1ne1  7709  znegclb  8034  iccneg  8607  fzsn  8679  fz1sbc  8708  fzofzp1b  8834  reim0b  9070  bj-om  9371
  Copyright terms: Public domain W3C validator