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

Theorem jcai 557
 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 553 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 196  df-an 385 This theorem is referenced by:  euan  2518  reu6  3362  f1ocnv2d  6784  onfin2  8037  nnoddn2prm  15354  isinitoi  16476  istermoi  16477  iszeroi  16482  mpfrcl  19339  cpmatelimp  20336  cpmatelimp2  20338  clwlkf1clwwlklem  26376  f1o3d  28813  oddpwdc  29743  altopthsn  31238  volsupnfl  32624  mbfresfi  32626  qirropth  36491  brcofffn  37349  lighneal  40066  clwlksf1clwwlklem  41275
 Copyright terms: Public domain W3C validator