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

Theorem dcbid 806
Description: Equivalence property for decidability. Deduction form. (Contributed by Jim Kingdon, 7-Sep-2019.)
Hypothesis
Ref Expression
dcbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
dcbid (𝜑 → (DECID 𝜓DECID 𝜒))

Proof of Theorem dcbid
StepHypRef Expression
1 dcbid.1 . . 3 (𝜑 → (𝜓𝜒))
21notbid 639 . . 3 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
31, 2orbi12d 765 . 2 (𝜑 → ((𝜓 ∨ ¬ 𝜓) ↔ (𝜒 ∨ ¬ 𝜒)))
4 df-dc 803 . 2 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
5 df-dc 803 . 2 (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
63, 4, 53bitr4g 222 1 (𝜑 → (DECID 𝜓DECID 𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104  wo 680  DECID wdc 802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681
This theorem depends on definitions:  df-bi 116  df-dc 803
This theorem is referenced by:  dcbiit  807  exmidexmid  4088  exmidel  4096  dcdifsnid  6366  finexdc  6762  undifdcss  6777  ssfirab  6788  fidcenumlemrks  6807  difinfsnlem  6950  difinfsn  6951  ctssdclemn0  6961  ctssdccl  6962  ctssdclemr  6963  ctssdc  6964  ltdcpi  7095  enqdc  7133  enqdc1  7134  ltdcnq  7169  fzodcel  9869  exfzdc  9957  sumeq1  11064  sumdc  11067  summodclem2  11091  summodc  11092  zsumdc  11093  fsum3  11096  isumz  11098  isumss  11100  fisumss  11101  isumss2  11102  fsum3cvg2  11103  fsumsersdc  11104  fsumsplit  11116  dvdsdc  11397  zdvdsdc  11410  zsupcllemstep  11534  infssuzex  11538  hashdvds  11792  ennnfonelemr  11831  ennnfonelemim  11832  ctinf  11838  ctiunctlemudc  11845  ctiunct  11848  sumdc2  12829  nninfsellemdc  13029
  Copyright terms: Public domain W3C validator