![]() |
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 903 | . 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑)) | |
2 | orbi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | orbi2i 943 | . 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
4 | orcom 903 | . 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
5 | 1, 3, 4 | 3bitri 289 | 1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∨ wo 880 |
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 199 df-or 881 |
This theorem is referenced by: orbi12i 945 orordi 959 3anorOLD 1136 3ianor 1138 3or6 1577 cadan 1724 nfnbiOLD 1957 19.45v 2101 19.45 2284 unass 3998 tz7.48lem 7803 dffin7-2 9536 zorng 9642 entri2 9696 grothprim 9972 leloe 10444 arch 11616 elznn0nn 11719 xrleloe 12264 swrdnnn0nd 13722 ressval3d 16301 ressval3dOLD 16302 opsrtoslem1 19845 fctop2 21181 alexsubALTlem3 22224 colinearalg 26210 numclwwlk3lem2 27800 disjnf 29932 ballotlemfc0 31101 ballotlemfcc 31102 noextenddif 32361 sleloe 32419 ordcmp 32980 poimirlem21 33975 ovoliunnfl 33996 biimpor 34426 tsim1 34478 leatb 35368 expdioph 38434 ifpim123g 38688 ifpimimb 38692 ifpororb 38693 rp-fakeinunass 38703 andi3or 39161 uneqsn 39162 sbc3or 39577 en3lpVD 39900 el1fzopredsuc 42224 iccpartgt 42252 fmtno4prmfac 42315 ldepspr 43110 |
Copyright terms: Public domain | W3C validator |