![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jcad | Unicode version |
Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Ref | Expression |
---|---|
jcad.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
jcad.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
jcad |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jcad.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jcad.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | pm3.2 138 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl6c 66 |
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-ia3 107 |
This theorem is referenced by: jca2 306 jctild 314 jctird 315 ancld 323 ancrd 324 anim12ii 341 equsex 1707 equsexd 1708 rexim 2529 rr19.28v 2828 sotricim 4253 sotritrieq 4255 ordsucss 4428 ordpwsucss 4490 peano5 4520 iss 4873 funssres 5173 ssimaex 5490 elpreima 5547 resflem 5592 tposfo2 6172 nnmord 6421 map0g 6590 mapsn 6592 enq0tr 7266 addnqprl 7361 addnqpru 7362 cauappcvgprlemdisj 7483 lttri3 7868 ltleap 8418 mulgt1 8645 nominpos 8981 uzind 9186 indstr 9415 eqreznegel 9433 shftuz 10621 caucvgrelemcau 10784 sqrtsq 10848 mulcn2 11113 dvdsgcdb 11737 algcvgblem 11766 lcmdvdsb 11801 rpexp 11867 cnntr 12433 cnrest2 12444 txlm 12487 metrest 12714 bj-om 13306 |
Copyright terms: Public domain | W3C validator |