![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3anim123i | Structured version Visualization version Unicode version |
Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anim123i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
3anim123i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3anim123i.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3anim123i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anim123i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant1 1028 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 3anim123i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | 3ad2ant2 1029 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3anim123i.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | 3ad2ant3 1030 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 2, 4, 6 | 3jca 1187 |
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 df-3an 986 |
This theorem is referenced by: 3anim1i 1193 3anim2i 1194 3anim3i 1195 syl3an 1309 syl3anl 1318 spc3egv 3137 eloprabga 6380 le2tri3i 9761 fzmmmeqm 11829 elfz1b 11861 elfz0fzfz0 11892 elfzmlbmOLD 11898 elfzmlbp 11899 elfzo1 11962 ssfzoulel 12002 flltdivnn0lt 12062 swrdswrd 12811 swrdccatin2 12838 swrdccat 12844 mulmoddvds 14356 nndvdslegcd 14472 ncoprmlnprm 14670 symg2hash 17031 pmtrdifellem2 17111 unitgrp 17888 isdrngd 17993 bcthlem5 22289 colinearalg 24933 axcontlem8 24994 usgra2adedgwlk 25335 rngosn 26125 chirredlem2 28037 rexdiv 28388 bnj944 29742 bnj969 29750 nnssi2 31108 nnssi3 31109 isdrngo2 32190 leatb 32852 paddasslem9 33387 paddasslem10 33388 dvhvaddass 34659 expgrowthi 36676 nnsum4primesodd 38885 nnsum4primesoddALTV 38886 cplgr3v 39485 2zrngasgrp 39927 2zrngmsgrp 39934 lincvalpr 40198 refdivmptf 40340 refdivmptfv 40344 |
Copyright terms: Public domain | W3C validator |