Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orbi1i | Structured version Visualization version GIF version |
Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
orbi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
orbi1i | ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom 870 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑)) | |
2 | orbi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | orbi2i 913 | . 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
4 | orcom 870 | . 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 300 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∨ wo 847 |
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 210 df-or 848 |
This theorem is referenced by: orbi12i 915 orordi 929 3ianor 1109 3or6 1449 norasslem1 1536 norass 1539 cadan 1616 19.45v 2002 19.45 2237 unass 4089 tz7.48lem 8186 dffin7-2 10025 zorng 10131 entri2 10185 grothprim 10461 leloe 10932 arch 12100 elznn0nn 12203 xrleloe 12747 swrdnnn0nd 14234 ressval3d 16811 opsrtoslem1 21025 fctop2 21915 alexsubALTlem3 22959 colinearalg 27014 numclwwlk3lem2 28480 disjnf 30641 ballotlemfc0 32184 ballotlemfcc 32185 satfvsucsuc 33053 satfbrsuc 33054 fmlasuc 33074 otthne 33411 noextenddif 33621 sleloe 33707 ordcmp 34386 wl-df2-3mintru2 35406 poimirlem21 35548 ovoliunnfl 35569 biimpor 35992 tsim1 36038 leatb 37056 metakunt1 39863 expdioph 40563 ifpim123g 40807 ifpimimb 40811 ifpororb 40812 rp-fakeinunass 40822 andi3or 41324 uneqsn 41325 sbc3or 41840 en3lpVD 42153 el1fzopredsuc 44505 iccpartgt 44567 fmtno4prmfac 44712 ldepspr 45502 |
Copyright terms: Public domain | W3C validator |