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

Theorem jcai 560
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 555 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  euan  2660  reu6  3528  f1ocnv2d  7043  onfin2  8309  nnoddn2prm  15710  isinitoi  16846  istermoi  16847  iszeroi  16852  mpfrcl  19712  cpmatelimp  20711  cpmatelimp2  20713  clwlksf1clwwlklemOLD  27214  f1o3d  29732  oddpwdc  30717  altopthsn  32366  volsupnfl  33759  mbfresfi  33761  qirropth  37967  brcofffn  38823  lighneal  42030
  Copyright terms: Public domain W3C validator