![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jccir | Structured version Visualization version GIF version |
Description: Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 27813. (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 507 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: jccil 518 oelim2 7942 trclfv 14118 maxprmfct 15792 telgsums 18744 chpmat1dlem 21010 chpdmatlem2 21014 leordtvallem1 21385 leordtvallem2 21386 mbfmax 23815 wlklnwwlkln2lem 27182 0wlkonlem1 27483 relowlpssretop 33750 ntrclsk13 39202 stoweidlem34 41038 smonoord 42222 |
Copyright terms: Public domain | W3C validator |