![]() |
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 512 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: euan 2621 euanv 2624 reu6 3682 f1ocnv2d 7598 onfin2 9133 nnoddn2prm 16637 isinitoi 17839 istermoi 17840 iszeroi 17849 mpfrcl 21441 cpmatelimp 22007 cpmatelimp2 22009 f1o3d 31386 oddpwdc 32782 altopthsn 34478 bj-animbi 34954 volsupnfl 36055 mbfresfi 36056 qirropth 41134 oacl2g 41565 omabs2 41566 omcl2 41567 ofoafg 41569 ofoafo 41571 naddcnff 41577 naddcnffo 41579 brcofffn 42208 lighneal 45698 |
Copyright terms: Public domain | W3C validator |