![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > exbiri | Structured version Unicode version |
Description: Inference form of exbir 31509. This proof is exbiriVD 31945 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof shortened by Wolf Lammen, 27-Jan-2013.) |
Ref | Expression |
---|---|
exbiri.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exbiri |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbiri.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpar 485 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exp31 604 |
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 185 df-an 371 |
This theorem is referenced by: biimp3ar 1320 eqrdavOLD 2453 tfrlem9 6957 sbthlem1 7534 addcanpr 9330 axpre-sup 9451 lbreu 10395 zmax 11065 uzsubsubfz 11592 elfzodifsumelfzo 11725 swrdccatin12lem3 12503 cshwidxmod 12562 ucnima 19998 usgraidx2vlem2 23489 mdslmd1lem1 25908 mdslmd1lem2 25909 dfon2 27772 cgrextend 28206 brsegle 28306 brabg2 28780 ralxfrd2 30308 elfzom1elp1fzo 30389 wwlkextwrd 30531 numclwlk1lem2f1 30858 |
Copyright terms: Public domain | W3C validator |