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 340 equsex 1706 equsexd 1707 rexim 2526 rr19.28v 2824 sotricim 4245 sotritrieq 4247 ordsucss 4420 ordpwsucss 4482 peano5 4512 iss 4865 funssres 5165 ssimaex 5482 elpreima 5539 resflem 5584 tposfo2 6164 nnmord 6413 map0g 6582 mapsn 6584 enq0tr 7242 addnqprl 7337 addnqpru 7338 cauappcvgprlemdisj 7459 lttri3 7844 ltleap 8394 mulgt1 8621 nominpos 8957 uzind 9162 indstr 9388 eqreznegel 9406 shftuz 10589 caucvgrelemcau 10752 sqrtsq 10816 mulcn2 11081 dvdsgcdb 11701 algcvgblem 11730 lcmdvdsb 11765 rpexp 11831 cnntr 12394 cnrest2 12405 txlm 12448 metrest 12675 bj-om 13135 |
Copyright terms: Public domain | W3C validator |