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

Theorem jcai 508
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 503 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  euan  2705  reu6  3604  f1ocnv2d  7126  onfin2  8401  nnoddn2prm  15753  isinitoi  16877  istermoi  16878  iszeroi  16883  mpfrcl  19746  cpmatelimp  20751  cpmatelimp2  20753  clwlksf1clwwlklemOLD  27265  f1o3d  29781  oddpwdc  30764  altopthsn  32411  volsupnfl  33786  mbfresfi  33787  qirropth  37992  brcofffn  38847  lighneal  42121
  Copyright terms: Public domain W3C validator