Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > jccir | Structured version Visualization version Unicode version |
Description: Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 27266. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.) |
Ref | Expression |
---|---|
jccir.1 | |
jccir.2 |
Ref | Expression |
---|---|
jccir |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jccir.1 | . 2 | |
2 | jccir.2 | . . 3 | |
3 | 1, 2 | syl 17 | . 2 |
4 | 1, 3 | jca 554 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: jccil 563 oelim2 7675 hashf1rnOLD 13143 trclfv 13741 maxprmfct 15421 telgsums 18390 chpmat1dlem 20640 chpdmatlem2 20644 leordtvallem1 21014 leordtvallem2 21015 mbfmax 23416 wlklnwwlkln2lem 26768 0wlkonlem1 26979 relowlpssretop 33212 ntrclsk13 38369 stoweidlem34 40251 smonoord 41341 |
Copyright terms: Public domain | W3C validator |