![]() |
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 215 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | orim2i 908 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
4 | 1 | biimpri 227 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | orim2i 908 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
6 | 3, 5 | impbii 208 | 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: orbi1i 911 orbi12i 912 orass 919 or4 924 or42 925 orordir 927 dn1 1055 dfifp6 1066 excxor 1510 nf3 1781 nfnbiOLD 1851 19.44v 1989 19.44 2226 sspsstri 4098 unass 4164 undi 4273 undif3 4289 2nreu 4438 undif4 4461 ssunpr 4833 sspr 4834 sstp 4835 pr1eqbg 4855 iinun2 5073 iinuni 5098 qfto 6125 somin1 6137 ordtri2 6403 on0eqel 6492 frxp 8132 poxp2 8149 soseq 8165 frrlem12 8304 wfrlem14OLD 8344 wfrlem15OLD 8345 supgtoreq 9506 wemapsolem 9586 fin1a2lem12 10445 psslinpr 11065 suplem2pr 11087 fimaxre 12204 elnn0 12520 elxnn0 12592 elnn1uz2 12955 elxr 13144 xrinfmss 13337 elfzp1 13599 hashf1lem2 14470 dvdslelem 16306 pythagtrip 16831 tosso 18439 maducoeval2 22630 madugsum 22633 ist0-3 23337 limcdif 25893 ellimc2 25894 limcmpt 25900 limcres 25903 plydivex 26322 taylfval 26383 precsexlem9 28211 legtrid 28515 legso 28523 lmicom 28712 numedglnl 29077 nb3grprlem2 29314 clwwlkneq0 29959 atomli 32312 atoml2i 32313 or3di 32386 disjnf 32490 disjex 32512 disjexc 32513 cycpmrn 33025 orngsqr 33187 ind1a 33865 esumcvg 33932 voliune 34075 volfiniune 34076 bnj964 34801 satfvsucsuc 35206 satfrnmapom 35211 satf0op 35218 fmlaomn0 35231 dfso2 35590 lineunray 35984 bj-dfbi4 36290 bj-axadj 36761 wl-ifpimpr 37186 wl-df4-3mintru2 37207 poimirlem18 37352 poimirlem23 37357 poimirlem27 37361 poimirlem31 37365 itg2addnclem2 37386 tsxo1 37851 tsxo2 37852 tsxo3 37853 tsxo4 37854 tsna1 37858 tsna2 37859 tsna3 37860 ts3an1 37864 ts3an2 37865 ts3an3 37866 ts3or1 37867 ts3or2 37868 ts3or3 37869 dfeldisj5 38432 aks4d1p7 41795 reelznn0nn 42160 dflim5 43032 ifpim123g 43204 ifpor123g 43212 rp-fakeoranass 43218 ontric3g 43226 frege133d 43469 or3or 43727 undif3VD 44595 wallispilem3 45724 iccpartgt 47035 nnsum4primeseven 47408 nnsum4primesevenALTV 47409 clnbupgrel 47441 lindslinindsimp2 47882 |
Copyright terms: Public domain | W3C validator |