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 866 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑)) | |
2 | orbi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | orbi2i 909 | . 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
4 | orcom 866 | . 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 296 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 843 |
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 206 df-or 844 |
This theorem is referenced by: orbi12i 911 orordi 925 3ianor 1105 3or6 1445 norasslem1 1532 norass 1535 cadan 1612 19.45v 1998 19.45 2234 unass 4096 tz7.48lem 8242 dffin7-2 10085 zorng 10191 entri2 10245 grothprim 10521 leloe 10992 arch 12160 elznn0nn 12263 xrleloe 12807 swrdnnn0nd 14297 ressval3d 16882 ressval3dOLD 16883 opsrtoslem1 21172 fctop2 22063 alexsubALTlem3 23108 colinearalg 27181 numclwwlk3lem2 28649 disjnf 30810 ballotlemfc0 32359 ballotlemfcc 32360 satfvsucsuc 33227 satfbrsuc 33228 fmlasuc 33248 otthne 33585 noextenddif 33798 sleloe 33884 ordcmp 34563 wl-df2-3mintru2 35583 poimirlem21 35725 ovoliunnfl 35746 biimpor 36169 tsim1 36215 leatb 37233 metakunt1 40053 expdioph 40761 ifpim123g 41005 ifpimimb 41009 ifpororb 41010 rp-fakeinunass 41020 andi3or 41521 uneqsn 41522 sbc3or 42041 en3lpVD 42354 el1fzopredsuc 44705 iccpartgt 44767 fmtno4prmfac 44912 ldepspr 45702 |
Copyright terms: Public domain | W3C validator |