| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > orbi2i | Structured version Visualization version GIF version | ||
| Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
| Ref | Expression |
|---|---|
| orbi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| orbi2i | ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orbi2i.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | 1 | biimpi 216 | . . 3 ⊢ (𝜑 → 𝜓) |
| 3 | 2 | orim2i 911 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
| 4 | 1 | biimpri 228 | . . 3 ⊢ (𝜓 → 𝜑) |
| 5 | 4 | orim2i 911 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
| 6 | 3, 5 | impbii 209 | 1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∨ wo 848 |
| 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 849 |
| This theorem is referenced by: orbi1i 914 orbi12i 915 orass 922 or4 927 or42 928 orordir 930 dn1 1058 dfifp6 1069 excxor 1516 nf3 1786 19.44v 1992 19.44 2237 sspsstri 4105 unass 4172 undi 4285 undif3 4300 2nreu 4444 undif4 4467 ssunpr 4834 sspr 4835 sstp 4836 pr1eqbg 4857 iinun2 5073 iinuni 5098 qfto 6141 somin1 6153 ordtri2 6419 on0eqel 6508 frxp 8151 poxp2 8168 soseq 8184 frrlem12 8322 wfrlem14OLD 8362 wfrlem15OLD 8363 supgtoreq 9510 wemapsolem 9590 fin1a2lem12 10451 psslinpr 11071 suplem2pr 11093 fimaxre 12212 elnn0 12528 elxnn0 12601 elnn1uz2 12967 elxr 13158 xrinfmss 13352 elfzp1 13614 hashf1lem2 14495 dvdslelem 16346 pythagtrip 16872 tosso 18464 maducoeval2 22646 madugsum 22649 ist0-3 23353 limcdif 25911 ellimc2 25912 limcmpt 25918 limcres 25921 plydivex 26339 taylfval 26400 precsexlem9 28239 legtrid 28599 legso 28607 lmicom 28796 numedglnl 29161 nb3grprlem2 29398 clwwlkneq0 30048 atomli 32401 atoml2i 32402 or3di 32478 disjnf 32583 disjex 32605 disjexc 32606 ind1a 32844 cycpmrn 33163 orngsqr 33334 esumcvg 34087 voliune 34230 volfiniune 34231 bnj964 34957 satfvsucsuc 35370 satfrnmapom 35375 satf0op 35382 fmlaomn0 35395 dfso2 35755 lineunray 36148 bj-dfbi4 36574 bj-axadj 37042 wl-ifpimpr 37467 wl-df4-3mintru2 37488 poimirlem18 37645 poimirlem23 37650 poimirlem27 37654 poimirlem31 37658 itg2addnclem2 37679 tsxo1 38144 tsxo2 38145 tsxo3 38146 tsxo4 38147 tsna1 38151 tsna2 38152 tsna3 38153 ts3an1 38157 ts3an2 38158 ts3an3 38159 ts3or1 38160 ts3or2 38161 ts3or3 38162 dfeldisj5 38722 aks4d1p7 42084 reelznn0nn 42479 dflim5 43342 ifpim123g 43513 ifpor123g 43521 rp-fakeoranass 43527 ontric3g 43535 frege133d 43778 or3or 44036 undif3VD 44902 wallispilem3 46082 iccpartgt 47414 nnsum4primeseven 47787 nnsum4primesevenALTV 47788 clnbupgrel 47821 usgrexmpl2trifr 47996 lindslinindsimp2 48380 |
| Copyright terms: Public domain | W3C validator |