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 208  df-an 397
This theorem is referenced by:  euan  2704  euanv  2707  reu6  3720  f1ocnv2d  7391  onfin2  8702  nnoddn2prm  16140  isinitoi  17255  istermoi  17256  iszeroi  17261  mpfrcl  20218  cpmatelimp  21236  cpmatelimp2  21238  f1o3d  30287  oddpwdc  31498  altopthsn  33306  bj-animbi  33778  volsupnfl  34804  mbfresfi  34805  qirropth  39366  brcofffn  40242  lighneal  43604
  Copyright terms: Public domain W3C validator