|   | 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 912 | . 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) | 
| 4 | orcom 870 | . 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
| 5 | 1, 3, 4 | 3bitri 297 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∨ 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 207 df-or 848 | 
| This theorem is referenced by: orbi12i 914 orordi 928 3ianor 1106 3or6 1448 norasslem1 1533 norass 1536 cadan 1608 19.45v 1992 19.45 2237 unass 4171 tz7.48lem 8482 dffin7-2 10439 zorng 10545 entri2 10599 grothprim 10875 leloe 11348 arch 12525 elznn0nn 12629 xrleloe 13187 swrdnnn0nd 14695 ressval3d 17293 opsrtoslem1 22080 fctop2 23013 alexsubALTlem3 24058 noextenddif 27714 sleloe 27800 precsexlem11 28242 eln0s 28359 colinearalg 28926 numclwwlk3lem2 30404 disjnf 32584 ballotlemfc0 34496 ballotlemfcc 34497 satfvsucsuc 35371 satfbrsuc 35372 fmlasuc 35392 ordcmp 36449 wl-df2-3mintru2 37487 poimirlem21 37649 ovoliunnfl 37670 biimpor 38092 tsim1 38138 leatb 39294 metakunt1 42207 expdioph 43040 dflim5 43347 ifpim123g 43518 ifpimimb 43522 ifpororb 43523 rp-fakeinunass 43533 andi3or 44042 uneqsn 44043 sbc3or 44557 en3lpVD 44870 el1fzopredsuc 47342 iccpartgt 47419 fmtno4prmfac 47564 dfvopnbgr2 47844 isubgr3stgrlem4 47941 ldepspr 48395 | 
| Copyright terms: Public domain | W3C validator |