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 137 | . 2 | |
4 | 1, 2, 3 | syl6c 65 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 |
This theorem is referenced by: jctild 309 jctird 310 ancld 318 ancrd 319 anim12ii 335 equsex 1656 equsexd 1657 rexim 2455 rr19.28v 2734 sotricim 4078 sotritrieq 4080 ordsucss 4248 ordpwsucss 4310 peano5 4339 iss 4674 funssres 4962 ssimaex 5255 elpreima 5307 tposfo2 5905 nnmord 6113 enq0tr 6624 addnqprl 6719 addnqpru 6720 cauappcvgprlemdisj 6841 lttri3 7191 ltleap 7730 mulgt1 7941 nominpos 8268 uzind 8458 indstr 8681 eqreznegel 8699 shftuz 9705 caucvgrelemcau 9866 sqrtsq 9930 mulcn2 10151 dvdsgcdb 10402 algcvgblem 10431 lcmdvdsb 10466 rpexp 10532 bj-om 10732 |
Copyright terms: Public domain | W3C validator |