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 515 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: euan 2622 euanv 2625 reu6 3639 f1ocnv2d 7458 onfin2 8871 nnoddn2prm 16364 isinitoi 17505 istermoi 17506 iszeroi 17515 mpfrcl 21045 cpmatelimp 21609 cpmatelimp2 21611 f1o3d 30681 oddpwdc 32033 altopthsn 34000 bj-animbi 34476 volsupnfl 35559 mbfresfi 35560 qirropth 40433 brcofffn 41318 lighneal 44736 |
Copyright terms: Public domain | W3C validator |