![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jcai | Structured version Visualization version Unicode 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 539 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: euan 2369 reu6 3238 f1ocnv2d 6546 onfin2 7789 isinitoi 15946 istermoi 15947 iszeroi 15952 mpfrcl 18789 cpmatelimp 19784 cpmatelimp2 19786 clwlkf1clwwlklem 25625 f1o3d 28277 oddpwdc 29235 altopthsn 30776 volsupnfl 32029 mbfresfi 32031 qirropth 35800 |
Copyright terms: Public domain | W3C validator |