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

Theorem jcai 558
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 554 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 197  df-an 386
This theorem is referenced by:  euan  2529  reu6  3377  f1ocnv2d  6839  onfin2  8096  nnoddn2prm  15440  isinitoi  16574  istermoi  16575  iszeroi  16580  mpfrcl  19437  cpmatelimp  20436  cpmatelimp2  20438  clwlksf1clwwlklem  26834  f1o3d  29272  oddpwdc  30194  altopthsn  31707  volsupnfl  33083  mbfresfi  33085  qirropth  36950  brcofffn  37808  lighneal  40824
  Copyright terms: Public domain W3C validator