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 540 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃)) |
3 | orbi12i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | orbi1i 541 | . 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃)) |
5 | 2, 4 | bitri 263 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∨ wo 382 |
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 196 df-or 384 |
This theorem is referenced by: pm4.78 604 andir 908 anddi 910 dfbi3 933 4exmid 977 cases 1004 3orbi123i 1245 3or6 1402 cadcoma 1542 neorian 2876 sspsstri 3671 rexun 3755 elsymdif 3811 symdif2 3814 indi 3832 unab 3853 dfnf5 3906 inundif 3998 dfpr2 4143 ssunsn 4300 ssunpr 4305 sspr 4306 sstp 4307 prneimg 4328 prnebg 4329 pwpr 4368 pwtp 4369 unipr 4385 uniun 4392 iunun 4540 iunxun 4541 brun 4633 zfpair 4831 opthneg 4876 propeqop 4895 pwunss 4943 opthprc 5089 xpeq0 5473 difxp 5477 ordtri2or3 5741 ftpg 6328 ordunpr 6918 mpt2xneldm 7225 tpostpos 7259 oarec 7529 brdom2 7871 modom 8046 dfsup2 8233 wemapsolem 8338 leweon 8717 kmlem16 8870 fin23lem40 9056 axpre-lttri 9865 nn0n0n1ge2b 11236 elnn0z 11267 fz0 12227 sqeqori 12838 hashtpg 13121 cbvsum 14273 cbvprod 14484 rpnnen2lem12 14793 lcmfpr 15178 pythagtriplem2 15360 pythagtrip 15377 mreexexd 16131 mreexexdOLD 16132 ppttop 20621 fixufil 21536 alexsubALTlem2 21662 alexsubALTlem3 21663 alexsubALTlem4 21664 dyaddisj 23170 ofpreima2 28849 odutos 28994 trleile 28997 smatrcl 29190 ordtconlem1 29298 sitgaddlemb 29737 quad3 30818 nepss 30854 dfso2 30897 dfon2lem4 30935 dfon2lem5 30936 nofulllem5 31105 dfon3 31169 brcup 31216 dfrdg4 31228 hfun 31455 bj-dfifc2 31734 bj-eltag 32158 bj-projun 32175 poimirlem22 32601 poimirlem31 32610 poimirlem32 32611 ispridl2 33007 smprngopr 33021 isdmn3 33043 sbcori 33081 tsbi4 33113 4atlem3 33900 elpadd 34103 paddasslem17 34140 cdlemg31b0N 35000 cdlemg31b0a 35001 cdlemh 35123 jm2.23 36581 ifpim123g 36864 ifpananb 36870 rp-isfinite6 36883 iunrelexp0 37013 clsk1indlem3 37361 aovov0bi 39925 zeoALTV 40119 divgcdoddALTV 40131 |
Copyright terms: Public domain | W3C validator |