![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anim12dan | Structured version Visualization version Unicode version |
Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.) |
Ref | Expression |
---|---|
anim12dan.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
anim12dan.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anim12dan |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12dan.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 440 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | anim12dan.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 440 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | anim12d 570 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | imp 435 |
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: isocnv 6246 isocnv3 6248 f1oiso2 6268 xpexr2 6761 f1o2ndf1 6931 fnwelem 6938 omword 7297 oeword 7317 swoso 7420 xpf1o 7760 zorn2lem6 8957 ltapr 9496 ltord1 10168 pc11 14878 imasaddfnlem 15483 imasaddflem 15485 pslem 16501 mhmpropd 16637 frmdsssubm 16694 ghmsub 16940 gasubg 17005 invrpropd 17975 mplcoe5lem 18740 evlseu 18788 znfld 19180 cygznlem3 19189 cpmatmcl 19792 tgclb 20035 innei 20190 txcn 20690 txflf 21070 qustgplem 21184 cfilresi 22314 volcn 22613 itg1addlem4 22706 dvlip 22994 plymullem1 23217 lgsdir2 24305 lgsdchr 24325 brbtwn2 24984 axcontlem7 25049 usgra2adedgwlkon 25392 fargshiftf1 25414 frgrancvvdeqlemB 25815 ghgrplem2OLD 26144 ghsubgolemOLD 26147 vcsub4 26244 nvaddsub4 26331 hhcno 27606 hhcnf 27607 unopf1o 27618 counop 27623 afsval 29537 ghomgsg 30360 ontopbas 31137 onsuct0 31150 heicant 32020 ftc1anclem6 32067 anim12da 32083 equivbnd2 32169 ismtybndlem 32183 ismrer1 32215 iccbnd 32217 xihopellsmN 34867 dihopellsm 34868 dvconstbi 36727 2f1fvneq 39054 mgmhmpropd 40058 |
Copyright terms: Public domain | W3C validator |