![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orbi12d | GIF version |
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
orbi12d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
orbi12d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
orbi12d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi12d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | orbi1d 738 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
3 | orbi12d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
4 | 3 | orbi2d 737 | . 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
5 | 2, 4 | bitrd 186 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∨ wo 662 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm4.39 769 dcbid 782 3orbi123d 1243 dfbi3dc 1329 eueq3dc 2767 sbcor 2859 sbcorg 2860 unjust 2977 elun 3114 ifbi 3377 elprg 3426 eltpg 3446 rabrsndc 3468 preq12bg 3573 swopolem 4068 soeq1 4078 sowlin 4083 ordtri2orexmid 4274 regexmidlemm 4283 regexmidlem1 4284 reg2exmidlema 4285 ordsoexmid 4313 ordtri2or2exmid 4322 nn0suc 4353 nndceq0 4365 0elnn 4366 soinxp 4436 fununi 4998 funcnvuni 4999 fun11iun 5178 unpreima 5324 isosolem 5494 xporderlem 5883 poxp 5884 frec0g 6046 freccllem 6051 frecfcllem 6053 frecsuclem 6055 frecsuc 6056 indpi 6594 ltexprlemloc 6859 addextpr 6873 ltsosr 7003 aptisr 7017 mulextsr1lem 7018 mulextsr1 7019 axpre-ltwlin 7111 axpre-apti 7113 axpre-mulext 7116 axltwlin 7247 axapti 7250 reapval 7743 reapti 7746 reapmul1lem 7761 reapmul1 7762 reapadd1 7763 reapneg 7764 reapcotr 7765 remulext1 7766 apreim 7770 apsym 7773 apcotr 7774 apadd1 7775 addext 7777 apneg 7778 nn1m1nn 8124 nn1gt1 8139 elznn0 8447 elz2 8500 nn0n0n1ge2b 8508 nneoor 8530 uztric 8721 ltxr 8927 fzsplit2 9145 uzsplit 9185 fzospliti 9262 fzouzsplit 9265 exbtwnzlemstep 9334 exbtwnzlemex 9336 qavgle 9345 frec2uzled 9511 sq11ap 9736 sqrt11ap 10062 abs00ap 10086 maxclpr 10246 minmax 10250 sumeq1 10330 sumeq2d 10334 sumeq2 10335 fz1f1o 10336 zeo3 10412 odd2np1lem 10416 dvdsprime 10648 coprm 10667 decidi 10756 bj-dcbi 10877 bj-nn0suc0 10903 bj-inf2vnlem2 10924 bj-nn0sucALT 10931 |
Copyright terms: Public domain | W3C validator |