![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anim1d | Structured version Visualization version Unicode version |
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
anim1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anim1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | idd 25 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12d 570 |
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-an 377 |
This theorem is referenced by: pm3.45 849 exdistrf 2168 2ax6elem 2279 mopick2 2370 ssrexf 3460 ssrexv 3462 ssdif 3536 ssrin 3625 reupick 3695 disjss1 4351 copsexg 4660 po3nr 4747 frss 4779 coss2 4969 ordsssuc2 5490 fununi 5631 dffv2 5922 extmptsuppeq 6927 onfununi 7047 oaass 7249 ssnnfi 7778 fiint 7835 fiss 7925 wemapsolem 8052 tcss 8215 ac6s 8901 reclem2pr 9460 qbtwnxr 11483 ico0 11672 icoshft 11745 2ffzeq 11903 clsslem 13059 r19.2uz 13425 infpn2 14868 prmgaplem4 15035 fthres2 15848 ablfacrplem 17709 monmat2matmon 19859 neiss 20136 uptx 20651 txcn 20652 nrmr0reg 20775 cnpflfi 21025 cnextcn 21093 caussi 22278 ovolsslem 22448 tgtrisegint 24555 inagswap 24892 cycliscrct 25370 numclwwlkovgelim 25829 shorth 26960 fmptss 28285 ordtconlem1 28737 omsmon 29132 omssubadd 29134 omsmonOLD 29136 omssubaddOLD 29138 mclsax 30213 poseq 30497 nodenselem5 30580 trisegint 30801 segcon2 30878 opnrebl2 30983 poimirlem30 31972 itg2addnclem 31995 itg2addnclem2 31996 fdc1 32077 totbndss 32111 ablo4pnp 32180 keridl 32267 dib2dim 34813 dih2dimbALTN 34815 dvh1dim 35012 mapdpglem2 35243 pell14qrss1234 35704 pell1qrss14 35716 rmxycomplete 35767 lnr2i 35977 rp-fakeanorass 36159 isprm7 36661 rfcnnnub 37354 nnsum4primes4 38975 nnsum4primesprm 38977 nnsum4primesgbe 38979 nnsum4primesle9 38981 propeqop 39092 2ffzoeq 39158 cyclisCrct 39873 |
Copyright terms: Public domain | W3C validator |