anim1d - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > anim1d		Structured version Visualization version Unicode version

Theorem anim1d 588

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)

**Hypothesis**
Ref	Expression
anim1d.1

**Assertion**
Ref	Expression
anim1d	$/\$ $/\$

**Proof of Theorem anim1d**
Step	Hyp	Ref	Expression
1		anim1d.1	. 2
2		idd 24	. 2
3	1, 2	anim12d 586	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384

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 197 df-an 386

This theorem is referenced by: pm3.45 879 exdistrf 2333 2ax6elem 2449 mopick2 2540 ssrexf 3665 ssrexv 3667 ssdif 3745 ssrin 3838 reupick 3911 disjss1 4626 copsexg 4956 propeqop 4970 po3nr 5049 frss 5081 coss2 5278 ordsssuc2 5814 fununi 5964 dffv2 6271 extmptsuppeq 7319 onfununi 7438 oaass 7641 ssnnfi 8179 fiint 8237 fiss 8330 wemapsolem 8455 tcss 8620 ac6s 9306 reclem2pr 9870 qbtwnxr 12031 ico0 12221 icoshft 12294 2ffzeq 12460 clsslem 13723 r19.2uz 14091 isprm7 15420 infpn2 15617 prmgaplem4 15758 fthres2 16592 ablfacrplem 18464 monmat2matmon 20629 neiss 20913 uptx 21428 txcn 21429 nrmr0reg 21552 cnpflfi 21803 cnextcn 21871 caussi 23095 ovolsslem 23252 tgtrisegint 25394 inagswap 25730 clwwlknp 26887 shorth 28154 mptssALT 29474 uzssico 29546 ordtconnlem1 29970 omsmon 30360 omssubadd 30362 mclsax 31466 poseq 31750 trisegint 32135 segcon2 32212 opnrebl2 32316 poimirlem30 33439 itg2addnclem 33461 itg2addnclem2 33462 fdc1 33542 totbndss 33576 ablo4pnp 33679 keridl 33831 dib2dim 36532 dih2dimbALTN 36534 dvh1dim 36731 mapdpglem2 36962 pell14qrss1234 37420 pell1qrss14 37432 rmxycomplete 37482 lnr2i 37686 rp-fakeanorass 37858 rfcnnnub 39195 2ffzoeq 41338 nnsum4primes4 41677 nnsum4primesprm 41679 nnsum4primesgbe 41681 nnsum4primesle9 41683