![]() |
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 868 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑)) | |
2 | orbi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | orbi2i 910 | . 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
4 | orcom 868 | . 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 296 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 845 |
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 846 |
This theorem is referenced by: orbi12i 912 orordi 926 3ianor 1104 3or6 1443 norasslem1 1527 norass 1530 cadan 1602 19.45v 1989 19.45 2226 unass 4164 tz7.48lem 8462 dffin7-2 10423 zorng 10529 entri2 10583 grothprim 10859 leloe 11332 arch 12502 elznn0nn 12605 xrleloe 13158 swrdnnn0nd 14642 ressval3d 17230 ressval3dOLD 17231 opsrtoslem1 22021 fctop2 22952 alexsubALTlem3 23997 noextenddif 27647 sleloe 27733 precsexlem11 28165 eln0s 28273 colinearalg 28793 numclwwlk3lem2 30266 disjnf 32439 ballotlemfc0 34243 ballotlemfcc 34244 satfvsucsuc 35106 satfbrsuc 35107 fmlasuc 35127 ordcmp 36062 wl-df2-3mintru2 37095 poimirlem21 37245 ovoliunnfl 37266 biimpor 37688 tsim1 37734 leatb 38894 metakunt1 41791 expdioph 42586 dflim5 42900 ifpim123g 43072 ifpimimb 43076 ifpororb 43077 rp-fakeinunass 43087 andi3or 43596 uneqsn 43597 sbc3or 44113 en3lpVD 44426 el1fzopredsuc 46843 iccpartgt 46904 fmtno4prmfac 47049 dfvopnbgr2 47325 ldepspr 47727 |
Copyright terms: Public domain | W3C validator |