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 864 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑)) | |
2 | orbi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | orbi2i 906 | . 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
4 | orcom 864 | . 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 298 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: orbi12i 908 orordi 922 3ianor 1099 3or6 1438 norasslem1 1521 norass 1524 cadan 1601 19.45v 1991 19.45 2230 unass 4139 tz7.48lem 8066 dffin7-2 9808 zorng 9914 entri2 9968 grothprim 10244 leloe 10715 arch 11882 elznn0nn 11983 xrleloe 12525 swrdnnn0nd 14006 ressval3d 16549 opsrtoslem1 20192 fctop2 21541 alexsubALTlem3 22585 colinearalg 26623 numclwwlk3lem2 28090 disjnf 30248 ballotlemfc0 31649 ballotlemfcc 31650 satfvsucsuc 32509 satfbrsuc 32510 fmlasuc 32530 noextenddif 33072 sleloe 33130 ordcmp 33692 poimirlem21 34794 ovoliunnfl 34815 biimpor 35243 tsim1 35289 leatb 36308 expdioph 39498 ifpim123g 39744 ifpimimb 39748 ifpororb 39749 rp-fakeinunass 39759 andi3or 40250 uneqsn 40251 sbc3or 40743 en3lpVD 41056 el1fzopredsuc 43402 iccpartgt 43464 fmtno4prmfac 43611 ldepspr 44456 |
Copyright terms: Public domain | W3C validator |