![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orbi12i | Structured version Visualization version GIF version |
Description: Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
orbi12i.1 | ⊢ (𝜑 ↔ 𝜓) |
orbi12i.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
orbi12i | ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi12i.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
2 | 1 | orbi2i 941 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃)) |
3 | orbi12i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | orbi1i 942 | . 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃)) |
5 | 2, 4 | bitri 267 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∨ wo 878 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 199 df-or 879 |
This theorem is referenced by: pm4.78 963 andir 1036 anddi 1038 cases 1069 cases2 1074 3orbi123i 1199 3or6 1575 cadcoma 1725 neorian 3093 sspsstri 3937 rexun 4022 elsymdif 4077 symdif2OLD 4085 indi 4105 unab 4125 dfnf5 4184 inundif 4271 dfpr2 4418 ssunsn 4579 ssunpr 4583 sspr 4584 sstp 4585 prneimg 4605 prnebg 4606 pwpr 4654 pwtp 4655 unipr 4673 uniun 4681 iunun 4827 iunxun 4828 brun 4926 zfpair 5127 opthneg 5172 propeqop 5195 pwunss 5247 opthprc 5404 xpeq0 5799 difxp 5803 ordtri2or3 6064 ftpg 6679 ordunpr 7292 mpt2xneldm 7608 tpostpos 7642 oarec 7914 brdom2 8258 modom 8436 dfsup2 8625 wemapsolem 8731 djuunxp 9067 leweon 9154 kmlem16 9309 fin23lem40 9495 axpre-lttri 10309 nn0n0n1ge2b 11693 elnn0z 11724 fz0 12656 sqeqori 13277 hashtpg 13563 swrdnnn0nd 13728 swrdnd0 13729 cbvsum 14809 cbvprod 15025 rpnnen2lem12 15335 lcmfpr 15720 pythagtriplem2 15900 pythagtrip 15917 mreexexd 16668 cnfldfunALT 20126 ppttop 21189 fixufil 22103 alexsubALTlem2 22229 alexsubALTlem3 22230 alexsubALTlem4 22231 dyaddisj 23769 clwwlkneq0 27374 ofpreima2 30011 odutos 30204 trleile 30207 smatrcl 30403 ordtconnlem1 30511 sitgaddlemb 30951 quad3 32104 nepss 32139 dfso2 32182 dfon2lem4 32224 dfon2lem5 32225 dfon3 32533 brcup 32580 dfrdg4 32592 hfun 32819 bj-dfifc2 33088 bj-eltag 33486 bj-projun 33503 bj-ismooredr2 33587 poimirlem22 33974 poimirlem31 33983 poimirlem32 33984 ispridl2 34378 smprngopr 34392 isdmn3 34414 sbcori 34451 tsbi4 34482 4atlem3 35670 elpadd 35873 paddasslem17 35910 cdlemg31b0N 36768 cdlemg31b0a 36769 cdlemh 36891 jm2.23 38405 ifpim123g 38686 ifpananb 38692 rp-isfinite6 38704 iunrelexp0 38834 clsk1indlem3 39180 aovov0bi 42096 zeoALTV 42429 divgcdoddALTV 42441 line2xlem 43319 |
Copyright terms: Public domain | W3C validator |