![]() |
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 763 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃)) |
3 | orbi12i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | orbi1i 764 | . 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃)) |
5 | 2, 4 | bitri 184 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: andir 820 anddi 822 3orbi123i 1191 3or6 1334 excxor 1389 19.33b2 1640 sbequilem 1849 sborv 1902 sbor 1966 r19.43 2648 rexun 3330 indi 3397 difindiss 3404 symdifxor 3416 unab 3417 dfpr2 3626 rabrsndc 3675 pwprss 3820 pwtpss 3821 unipr 3838 uniun 3843 iunun 3980 iunxun 3981 brun 4069 pwunss 4298 ordsoexmid 4576 onintexmid 4587 dcextest 4595 opthprc 4692 cnvsom 5187 ftpg 5717 tpostpos 6284 eldju 7092 djur 7093 ltexprlemloc 7631 axpre-ltwlin 7907 axpre-apti 7909 axpre-mulext 7912 axpre-suploc 7926 fz01or 10136 cbvsum 11395 fsum3 11422 cbvprod 11593 fprodseq 11618 gcdsupex 11985 gcdsupcl 11986 pythagtriplem2 12293 pythagtrip 12310 |
Copyright terms: Public domain | W3C validator |