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: wi 4 wa 103 |
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 1721 equsexd 1722 rexim 2564 rr19.28v 2870 sotricim 4306 sotritrieq 4308 ordsucss 4486 ordpwsucss 4549 peano5 4580 iss 4935 funssres 5238 ssimaex 5555 elpreima 5613 resflem 5658 tposfo2 6244 nnmord 6494 map0g 6664 mapsn 6666 enq0tr 7389 addnqprl 7484 addnqpru 7485 cauappcvgprlemdisj 7606 lttri3 7992 ltleap 8544 mulgt1 8772 nominpos 9108 uzind 9316 indstr 9545 eqreznegel 9566 shftuz 10774 caucvgrelemcau 10937 sqrtsq 11001 mulcn2 11268 dvdsgcdb 11961 algcvgblem 11996 lcmdvdsb 12031 rpexp 12100 infpnlem1 12304 cnntr 12984 cnrest2 12995 txlm 13038 metrest 13265 bj-om 13937 |
Copyright terms: Public domain | W3C validator |