![]() |
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 302 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | syl112anc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 1, 2, 5, 6 | syl3anc 1184 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: fvun1 5419 caseinl 6891 caseinr 6892 reapmul1 8223 recrecap 8330 rec11rap 8332 divdivdivap 8334 dmdcanap 8343 ddcanap 8347 rerecclap 8351 div2negap 8356 divap1d 8422 divmulapd 8433 apdivmuld 8434 divmulap2d 8445 divmulap3d 8446 divassapd 8447 div12apd 8448 div23apd 8449 divdirapd 8450 divsubdirapd 8451 div11apd 8452 ltmul12a 8476 ltdiv1 8484 ltrec 8499 lt2msq1 8501 lediv2 8507 lediv23 8509 recp1lt1 8515 qapne 9281 xadd4d 9509 xleaddadd 9511 modqge0 9946 modqlt 9947 modqid 9963 expgt1 10172 nnlesq 10237 expnbnd 10256 facubnd 10332 resqrexlemover 10622 mulcn2 10920 cvgratnnlemnexp 11132 cvgratnnlemmn 11133 eftlub 11194 eflegeo 11206 sin01bnd 11262 cos01bnd 11263 eirraplem 11278 bezoutlemnewy 11477 bezoutlemstep 11478 mulgcd 11497 mulgcddvds 11568 prmind2 11594 oddpwdclemxy 11639 oddpwdclemodd 11642 qnumgt0 11668 txdis 12227 txdis1cn 12228 xblm 12345 |
Copyright terms: Public domain | W3C validator |