MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jcai Unicode version

Theorem jcai 536
Description: Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)
Hypotheses
Ref Expression
jcai.1
jcai.2
Assertion
Ref Expression
jcai

Proof of Theorem jcai
StepHypRef Expression
1 jcai.1 . 2
2 jcai.2 . . 3
31, 2mpd 15 . 2
41, 3jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  euan  2351  reu6  3288  f1ocnv2d  6526  onfin2  7729  mpfrcl  18187  cpmatelimp  19213  cpmatelimp2  19215  clwlkf1clwwlklem  24849  f1o3d  27471  oddpwdc  28293  altopthsn  29611  volsupnfl  30059  mbfresfi  30061  qirropth  30844  isinitoi  32609  istermoi  32610  iszeroi  32615
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 185  df-an 371
  Copyright terms: Public domain W3C validator