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  2617  euanv  2620  reu6  3719  f1ocnv2d  7643  onfin2  9216  nnoddn2prm  16728  isinitoi  17933  istermoi  17934  iszeroi  17943  mpfrcl  21579  cpmatelimp  22145  cpmatelimp2  22147  f1o3d  31783  oddpwdc  33248  altopthsn  34827  bj-animbi  35303  volsupnfl  36401  mbfresfi  36402  qirropth  41481  oacl2g  41915  omabs2  41917  omcl2  41918  ofoafg  41939  ofoafo  41941  naddcnff  41947  naddcnffo  41949  brcofffn  42617  lighneal  46115
  Copyright terms: Public domain W3C validator