![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > anim12dan | Structured 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 434 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | anim12dan.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 434 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | anim12d 563 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | imp 429 |
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 185 df-an 371 |
This theorem is referenced by: isocnv 6120 isocnv3 6122 f1oiso2 6142 xpexr2 6619 f1o2ndf1 6780 fnwelem 6787 omword 7109 oeword 7129 swoso 7232 xpf1o 7573 zorn2lem6 8771 ltapr 9315 ltord1 9967 pc11 14048 imasaddfnlem 14568 imasaddflem 14570 pslem 15478 mhmpropd 15572 frmdsssubm 15641 ghmsub 15857 gasubg 15922 invrpropd 16896 mplcoe5lem 17654 evlseu 17709 znfld 18102 cygznlem3 18111 tgclb 18691 innei 18845 txcn 19315 txflf 19695 divstgplem 19807 cfilresi 20922 volcn 21202 itg1addlem4 21293 dvlip 21581 plymullem1 21798 lgsdir2 22783 lgsdchr 22803 brbtwn2 23286 axcontlem7 23351 fargshiftf1 23658 ghgrplem2 23989 ghsubgolem 23992 vcsub4 24089 nvaddsub4 24176 hhcno 25443 hhcnf 25444 unopf1o 25455 counop 25460 ghomgsg 27446 ontopbas 28408 onsuct0 28421 heicant 28564 ftc1anclem6 28610 anim12da 28742 equivbnd2 28829 ismtybndlem 28843 ismrer1 28875 iccbnd 28877 dvconstbi 29746 2f1fvneq 30281 usgra2adedgwlkon 30445 frgrancvvdeqlemB 30769 cpmatmcl 31182 xihopellsmN 35205 dihopellsm 35206 |
Copyright terms: Public domain | W3C validator |