![]() |
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 501 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 |
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 383 |
This theorem is referenced by: euan 2679 reu6 3547 f1ocnv2d 7037 onfin2 8312 nnoddn2prm 15723 isinitoi 16860 istermoi 16861 iszeroi 16866 mpfrcl 19733 cpmatelimp 20737 cpmatelimp2 20739 clwlksf1clwwlklemOLD 27249 f1o3d 29771 oddpwdc 30756 altopthsn 32405 volsupnfl 33786 mbfresfi 33787 qirropth 37997 brcofffn 38853 lighneal 42051 |
Copyright terms: Public domain | W3C validator |