![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orbi2i | Structured version Visualization version Unicode 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 199 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | orim2i 525 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 211 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | orim2i 525 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 192 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-or 376 |
This theorem is referenced by: orbi1i 527 orbi12i 528 orass 531 or4 535 or42 536 orordir 538 dn1 983 3orcomb 1001 excxor 1421 dfifp6 1441 19.44v 1838 nf4 2053 19.44 2059 r19.30 2946 sspsstri 3546 unass 3602 undi 3701 undif3 3715 undif4 3832 ssunpr 4146 sspr 4147 sstp 4148 iinun2 4357 iinuni 4378 qfto 5239 somin1 5251 ordtri2 5476 on0eqel 5558 frxp 6932 wfrlem14 7074 wfrlem15 7075 supgtoreq 8011 wemapsolem 8090 fin1a2lem12 8866 psslinpr 9481 suplem2pr 9503 fimaxre 10578 elnn0 10899 elnn1uz2 11263 elxr 11444 xrinfmss 11623 elfzp1 11874 hashf1lem2 12651 dvdslelem 14397 pythagtrip 14832 tosso 16330 maducoeval2 19713 madugsum 19716 ist0-3 20409 limcdif 22879 ellimc2 22880 limcmpt 22886 limcres 22889 plydivex 23298 taylfval 23362 legtrid 24684 legso 24692 lmicom 24878 nb3graprlem2 25228 numclwwlk3lem 25884 atomli 28083 atoml2i 28084 or3di 28149 disjnf 28229 disjex 28250 disjexc 28251 orngsqr 28615 ind1a 28890 esumcvg 28955 voliune 29100 volfiniune 29101 bnj964 29802 dfso2 30442 socnv 30453 soseq 30540 lineunray 30962 bj-dfbi4 31193 bj-nf3 31237 poimirlem18 32002 poimirlem23 32007 poimirlem27 32011 poimirlem31 32015 itg2addnclem2 32038 tsxo1 32423 tsxo2 32424 tsxo3 32425 tsxo4 32426 tsna1 32430 tsna2 32431 tsna3 32432 ts3an1 32436 ts3an2 32437 ts3an3 32438 ts3or1 32439 ts3or2 32440 ts3or3 32441 prtlem90 32475 ifpim123g 36188 ifpor123g 36196 rp-fakeoranass 36202 frege133d 36401 undif3VD 37318 wallispilem3 37966 iccpartgt 38778 nnsum4primeseven 38932 nnsum4primesevenALTV 38933 pr1eqbg 39030 elxnn0 39117 nb3grprlem2 39504 lindslinindsimp2 40528 |
Copyright terms: Public domain | W3C validator |