![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anim2d | Structured version Visualization version Unicode version |
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
anim1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anim2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 25 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | anim1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12d 566 |
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 189 df-an 373 |
This theorem is referenced by: eleq2dOLD 2514 moeq3 3214 ssel 3425 sscon 3566 uniss 4218 trel3 4504 ssopab2 4726 coss1 4989 fununi 5647 imadif 5656 fss 5735 ssimaex 5928 opabbrexOLD 6331 ssoprab2 6344 poxp 6905 soxp 6906 pmss12g 7495 ss2ixp 7532 xpdom2 7664 fisup2g 7981 fisupcl 7982 fiinf2g 8013 inf3lem1 8130 epfrs 8212 cfub 8676 cflm 8677 fin23lem34 8773 isf32lem2 8781 axcc4 8866 domtriomlem 8869 ltexprlem3 9460 nnunb 10862 indstr 11224 qbtwnxr 11490 qsqueeze 11491 xrsupsslem 11589 xrinfmsslem 11590 ioc0 11680 climshftlem 13631 o1rlimmul 13675 ramub2 14964 monmat2matmon 19841 tgcl 19978 neips 20122 ssnei2 20125 tgcnp 20262 cnpnei 20273 cnpco 20276 hauscmplem 20414 hauscmp 20415 llyss 20487 nllyss 20488 lfinun 20533 kgen2ss 20563 txcnpi 20616 txcmplem1 20649 fgss 20881 cnpflf2 21008 fclsss1 21030 fclscf 21033 alexsubALT 21059 cnextcn 21075 tsmsxp 21162 mopni3 21502 psmetutop 21575 iscau4 22242 caussi 22260 ovolgelb 22426 mbfi1flim 22674 ellimc3 22827 lhop1 22959 tgbtwndiff 24543 axcontlem4 24990 iswlkg 25245 sspmval 26365 sspival 26370 shmodsi 27035 atcvat4i 28043 cdj3lem2b 28083 ifeqeqx 28151 acunirnmpt 28254 xrge0infss 28333 crefss 28669 issgon 28938 cvmlift2lem12 30030 ss2mcls 30199 poseq 30484 btwndiff 30787 seglecgr12im 30870 fnessref 31006 waj-ax 31067 lukshef-ax2 31068 icorempt2 31747 finxpreclem1 31774 tan2h 31930 poimirlem31 31964 poimir 31966 mblfinlem3 31972 mblfinlem4 31973 ismblfin 31974 cvrat4 33002 athgt 33015 ps-2 33037 paddss1 33376 paddss2 33377 cdlemg33b0 34262 cdlemg33a 34267 dihjat1lem 34990 fphpdo 35654 irrapxlem2 35661 pell14qrss1234 35696 pell1qrss14 35708 acongtr 35822 ax6e2eq 36918 islptre 37693 limccog 37694 |
Copyright terms: Public domain | W3C validator |