![]() |
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 304 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | syl112anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 2, 5, 6 | syl3anc 1217 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: fvun1 5495 caseinl 6984 caseinr 6985 reapmul1 8381 recrecap 8493 rec11rap 8495 divdivdivap 8497 dmdcanap 8506 ddcanap 8510 rerecclap 8514 div2negap 8519 divap1d 8585 divmulapd 8596 apdivmuld 8597 divmulap2d 8608 divmulap3d 8609 divassapd 8610 div12apd 8611 div23apd 8612 divdirapd 8613 divsubdirapd 8614 div11apd 8615 ltmul12a 8642 ltdiv1 8650 ltrec 8665 lt2msq1 8667 lediv2 8673 lediv23 8675 recp1lt1 8681 qapne 9458 xadd4d 9698 xleaddadd 9700 modqge0 10136 modqlt 10137 modqid 10153 expgt1 10362 nnlesq 10427 expnbnd 10446 facubnd 10523 resqrexlemover 10814 mulcn2 11113 cvgratnnlemnexp 11325 cvgratnnlemmn 11326 eftlub 11433 eflegeo 11444 sin01bnd 11500 cos01bnd 11501 eirraplem 11519 bezoutlemnewy 11720 bezoutlemstep 11721 mulgcd 11740 mulgcddvds 11811 prmind2 11837 oddpwdclemxy 11883 oddpwdclemodd 11886 qnumgt0 11912 txdis 12485 txdis1cn 12486 xblm 12625 reeff1oleme 12901 tangtx 12967 cosordlem 12978 logdivlti 13010 apcxp2 13066 apdifflemr 13415 |
Copyright terms: Public domain | W3C validator |