![]() |
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 208 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | orim2i 894 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
4 | 1 | biimpri 220 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | orim2i 894 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
6 | 3, 5 | impbii 201 | 1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∨ wo 833 |
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 834 |
This theorem is referenced by: orbi1i 897 orbi12i 898 orass 905 or4 910 or42 911 orordir 913 dn1 1038 dfifp6 1049 excxor 1493 nf3 1749 nfnbi 1817 19.44v 1949 19.44 2170 r19.30OLD 3280 sspsstri 3969 unass 4031 undi 4138 undif3 4152 2nreu 4276 undif4 4299 ssunpr 4639 sspr 4640 sstp 4641 pr1eqbg 4661 iinun2 4861 iinuni 4886 qfto 5821 somin1 5833 ordtri2 6064 on0eqel 6146 frxp 7625 wfrlem14 7772 wfrlem15 7773 supgtoreq 8729 wemapsolem 8809 fin1a2lem12 9631 psslinpr 10251 suplem2pr 10273 fimaxre 11385 fimaxreOLD 11386 elnn0 11709 elxnn0 11781 elnn1uz2 12139 elxr 12328 xrinfmss 12519 elfzp1 12773 hashf1lem2 13627 dvdslelem 15519 pythagtrip 16027 tosso 17504 maducoeval2 20953 madugsum 20956 ist0-3 21657 limcdif 24177 ellimc2 24178 limcmpt 24184 limcres 24187 plydivex 24589 taylfval 24650 legtrid 26079 legso 26087 lmicom 26276 numedglnl 26632 nb3grprlem2 26866 clwwlkneq0 27544 atomli 29940 atoml2i 29941 or3di 30006 disjnf 30087 disjex 30108 disjexc 30109 orngsqr 30562 ind1a 30928 esumcvg 30995 voliune 31139 volfiniune 31140 bnj964 31868 satf0op 32193 dfso2 32516 soseq 32623 frrlem12 32661 lineunray 33135 bj-dfbi4 33429 poimirlem18 34357 poimirlem23 34362 poimirlem27 34366 poimirlem31 34370 itg2addnclem2 34391 tsxo1 34865 tsxo2 34866 tsxo3 34867 tsxo4 34868 tsna1 34872 tsna2 34873 tsna3 34874 ts3an1 34878 ts3an2 34879 ts3an3 34880 ts3or1 34881 ts3or2 34882 ts3or3 34883 dfeldisj5 35405 ifpim123g 39268 ifpor123g 39276 rp-fakeoranass 39282 frege133d 39479 or3or 39740 undif3VD 40641 wallispilem3 41789 iccpartgt 42965 nnsum4primeseven 43339 nnsum4primesevenALTV 43340 lindslinindsimp2 43891 |
Copyright terms: Public domain | W3C validator |