![]() |
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 910 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
4 | 1 | biimpri 227 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | orim2i 910 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
6 | 3, 5 | impbii 208 | 1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 |
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 847 |
This theorem is referenced by: orbi1i 913 orbi12i 914 orass 921 or4 926 or42 927 orordir 929 dn1 1057 dfifp6 1068 excxor 1516 nf3 1789 nfnbiOLD 1859 19.44v 1997 19.44 2231 sspsstri 4100 unass 4164 undi 4272 undif3 4288 2nreu 4439 undif4 4464 ssunpr 4833 sspr 4834 sstp 4835 pr1eqbg 4855 iinun2 5074 iinuni 5099 qfto 6118 somin1 6130 ordtri2 6395 on0eqel 6484 frxp 8106 poxp2 8123 soseq 8139 frrlem12 8276 wfrlem14OLD 8316 wfrlem15OLD 8317 supgtoreq 9460 wemapsolem 9540 fin1a2lem12 10401 psslinpr 11021 suplem2pr 11043 fimaxre 12153 elnn0 12469 elxnn0 12541 elnn1uz2 12904 elxr 13091 xrinfmss 13284 elfzp1 13546 hashf1lem2 14412 dvdslelem 16247 pythagtrip 16762 tosso 18367 maducoeval2 22123 madugsum 22126 ist0-3 22830 limcdif 25374 ellimc2 25375 limcmpt 25381 limcres 25384 plydivex 25791 taylfval 25852 precsexlem9 27640 legtrid 27821 legso 27829 lmicom 28018 numedglnl 28383 nb3grprlem2 28617 clwwlkneq0 29261 atomli 31612 atoml2i 31613 or3di 31678 disjnf 31778 disjex 31800 disjexc 31801 cycpmrn 32279 orngsqr 32390 ind1a 32954 esumcvg 33021 voliune 33164 volfiniune 33165 bnj964 33891 satfvsucsuc 34293 satfrnmapom 34298 satf0op 34305 fmlaomn0 34318 dfso2 34662 lineunray 35056 bj-dfbi4 35387 bj-axadj 35859 wl-ifpimpr 36284 wl-df4-3mintru2 36305 poimirlem18 36443 poimirlem23 36448 poimirlem27 36452 poimirlem31 36456 itg2addnclem2 36477 tsxo1 36942 tsxo2 36943 tsxo3 36944 tsxo4 36945 tsna1 36949 tsna2 36950 tsna3 36951 ts3an1 36955 ts3an2 36956 ts3an3 36957 ts3or1 36958 ts3or2 36959 ts3or3 36960 dfeldisj5 37528 aks4d1p7 40885 reelznn0nn 41265 dflim5 42011 ifpim123g 42183 ifpor123g 42191 rp-fakeoranass 42197 ontric3g 42205 frege133d 42448 or3or 42706 undif3VD 43575 wallispilem3 44717 iccpartgt 46029 nnsum4primeseven 46402 nnsum4primesevenALTV 46403 lindslinindsimp2 47045 |
Copyright terms: Public domain | W3C validator |