![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orbi12i | GIF version |
Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
orbi12i.1 | ⊢ (𝜑 ↔ 𝜓) |
orbi12i.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
orbi12i | ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi12i.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
2 | 1 | orbi2i 720 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃)) |
3 | orbi12i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | orbi1i 721 | . 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃)) |
5 | 2, 4 | bitri 183 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 670 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: andir 774 anddi 776 dcbii 791 3orbi123i 1139 3or6 1269 excxor 1324 19.33b2 1576 sbequilem 1777 sborv 1829 sbor 1888 r19.43 2547 rexun 3203 indi 3270 difindiss 3277 symdifxor 3289 unab 3290 dfpr2 3493 rabrsndc 3538 pwprss 3679 pwtpss 3680 unipr 3697 uniun 3702 iunun 3838 iunxun 3839 brun 3921 pwunss 4143 ordsoexmid 4415 onintexmid 4425 dcextest 4433 opthprc 4528 cnvsom 5018 ftpg 5536 tpostpos 6091 eldju 6868 djur 6869 ltexprlemloc 7316 axpre-ltwlin 7568 axpre-apti 7570 axpre-mulext 7573 fz01or 9732 cbvsum 10968 fsum3 10995 gcdsupex 11441 gcdsupcl 11442 |
Copyright terms: Public domain | W3C validator |