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 4308 sotritrieq 4310 ordsucss 4488 ordpwsucss 4551 peano5 4582 iss 4937 funssres 5240 ssimaex 5557 elpreima 5615 resflem 5660 tposfo2 6246 nnmord 6496 map0g 6666 mapsn 6668 enq0tr 7396 addnqprl 7491 addnqpru 7492 cauappcvgprlemdisj 7613 lttri3 7999 ltleap 8551 mulgt1 8779 nominpos 9115 uzind 9323 indstr 9552 eqreznegel 9573 shftuz 10781 caucvgrelemcau 10944 sqrtsq 11008 mulcn2 11275 dvdsgcdb 11968 algcvgblem 12003 lcmdvdsb 12038 rpexp 12107 infpnlem1 12311 cnntr 13019 cnrest2 13030 txlm 13073 metrest 13300 bj-om 13972 |
Copyright terms: Public domain | W3C validator |