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

Theorem jcai 517
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 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