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

Theorem jcai 518
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 513 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  euan  2618  euanv  2621  reu6  3720  f1ocnv2d  7646  onfin2  9219  nnoddn2prm  16731  isinitoi  17936  istermoi  17937  iszeroi  17946  mpfrcl  21617  cpmatelimp  22183  cpmatelimp2  22185  f1o3d  31820  oddpwdc  33284  altopthsn  34864  bj-animbi  35340  volsupnfl  36438  mbfresfi  36439  qirropth  41517  oacl2g  41951  omabs2  41953  omcl2  41954  ofoafg  41975  ofoafo  41977  naddcnff  41983  naddcnffo  41985  brcofffn  42653  lighneal  46152
  Copyright terms: Public domain W3C validator