![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl112anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.4 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl112anc.5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl112anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sylXanc.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | sylXanc.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | jca 300 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | syl112anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 2, 5, 6 | syl3anc 1170 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: fvun1 5313 reapmul1 7970 recrecap 8072 rec11rap 8074 divdivdivap 8076 dmdcanap 8085 ddcanap 8089 rerecclap 8093 div2negap 8098 divap1d 8163 divmulapd 8174 divmulap2d 8185 divmulap3d 8186 divassapd 8187 div12apd 8188 div23apd 8189 divdirapd 8190 divsubdirapd 8191 div11apd 8192 ltmul12a 8213 ltdiv1 8221 ltrec 8236 lt2msq1 8238 lediv2 8244 lediv23 8246 recp1lt1 8252 qapne 9017 modqge0 9626 modqlt 9627 modqid 9643 expgt1 9828 nnlesq 9892 expnbnd 9910 facubnd 9986 resqrexlemover 10268 mulcn2 10523 bezoutlemnewy 10763 bezoutlemstep 10764 mulgcd 10783 mulgcddvds 10854 prmind2 10880 oddpwdclemxy 10925 oddpwdclemodd 10928 qnumgt0 10954 |
Copyright terms: Public domain | W3C validator |