![]() |
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 306 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | syl112anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 2, 5, 6 | syl3anc 1249 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: fvun1 5599 caseinl 7115 caseinr 7116 reapmul1 8577 recrecap 8691 rec11rap 8693 divdivdivap 8695 dmdcanap 8704 ddcanap 8708 rerecclap 8712 div2negap 8717 divap1d 8783 divmulapd 8794 apdivmuld 8795 divmulap2d 8806 divmulap3d 8807 divassapd 8808 div12apd 8809 div23apd 8810 divdirapd 8811 divsubdirapd 8812 div11apd 8813 ltmul12a 8842 ltdiv1 8850 ltrec 8865 lt2msq1 8867 lediv2 8873 lediv23 8875 recp1lt1 8881 qapne 9664 xadd4d 9910 xleaddadd 9912 modqge0 10358 modqlt 10359 modqid 10375 expgt1 10584 nnlesq 10650 expnbnd 10670 facubnd 10752 resqrexlemover 11046 mulcn2 11347 cvgratnnlemnexp 11559 cvgratnnlemmn 11560 eftlub 11725 eflegeo 11736 sin01bnd 11792 cos01bnd 11793 eirraplem 11811 bezoutlemnewy 12024 bezoutlemstep 12025 mulgcd 12044 mulgcddvds 12121 prmind2 12147 oddpwdclemxy 12196 oddpwdclemodd 12199 qnumgt0 12225 pcpremul 12320 fldivp1 12375 pcfaclem 12376 qexpz 12379 prmpwdvds 12382 pockthg 12384 4sqlem10 12414 4sqlem12 12429 4sqlem16 12433 4sqlem17 12434 ablsub4 13245 txdis 14214 txdis1cn 14215 xblm 14354 reeff1oleme 14630 tangtx 14696 cosordlem 14707 logdivlti 14739 apcxp2 14795 lgsdilem 14865 lgseisenlem1 14887 lgseisenlem2 14888 2sqlem3 14901 2sqlem8 14907 apdifflemr 15233 |
Copyright terms: Public domain | W3C validator |