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

Theorem jcai 506
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 501 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  euan  2679  reu6  3547  f1ocnv2d  7037  onfin2  8312  nnoddn2prm  15723  isinitoi  16860  istermoi  16861  iszeroi  16866  mpfrcl  19733  cpmatelimp  20737  cpmatelimp2  20739  clwlksf1clwwlklemOLD  27249  f1o3d  29771  oddpwdc  30756  altopthsn  32405  volsupnfl  33786  mbfresfi  33787  qirropth  37997  brcofffn  38853  lighneal  42051
  Copyright terms: Public domain W3C validator