Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > jcai | Structured version Visualization version GIF version |
Description: Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.) |
Ref | Expression |
---|---|
jcai.1 | ⊢ (𝜑 → 𝜓) |
jcai.2 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
jcai | ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jcai.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | jcai.2 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | mpd 15 | . 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: euan 2530 reu6 3395 f1ocnv2d 6886 onfin2 8152 nnoddn2prm 15516 isinitoi 16653 istermoi 16654 iszeroi 16659 mpfrcl 19518 cpmatelimp 20517 cpmatelimp2 20519 clwlksf1clwwlklem 26968 f1o3d 29431 oddpwdc 30416 altopthsn 32068 volsupnfl 33454 mbfresfi 33456 qirropth 37473 brcofffn 38329 lighneal 41528 |
Copyright terms: Public domain | W3C validator |