Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > r19.29af | Structured version Visualization version Unicode version |
Description: A commonly used pattern based on r19.29 3072. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
Ref | Expression |
---|---|
r19.29af.0 | |
r19.29af.1 | |
r19.29af.2 |
Ref | Expression |
---|---|
r19.29af |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.29af.0 | . 2 | |
2 | nfv 1843 | . 2 | |
3 | r19.29af.1 | . 2 | |
4 | r19.29af.2 | . 2 | |
5 | 1, 2, 3, 4 | r19.29af2 3075 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wnf 1708 wcel 1990 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ex 1705 df-nf 1710 df-ral 2917 df-rex 2918 |
This theorem is referenced by: r19.29an 3077 r19.29a 3078 elsnxpOLD 5678 fsnex 6538 neiptopnei 20936 neitr 20984 utopsnneiplem 22051 isucn2 22083 foresf1o 29343 fsumiunle 29575 2sqmo 29649 reff 29906 locfinreflem 29907 ordtconnlem1 29970 esumrnmpt2 30130 esumgect 30152 esum2dlem 30154 esum2d 30155 esumiun 30156 sigapildsys 30225 oms0 30359 eulerpartlemgvv 30438 breprexplema 30708 stoweidlem27 40244 stoweidlem35 40252 |
Copyright terms: Public domain | W3C validator |