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

Theorem jcai 520
 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 515 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  euan  2683  euanv  2686  reu6  3667  f1ocnv2d  7389  onfin2  8713  nnoddn2prm  16158  isinitoi  17275  istermoi  17276  iszeroi  17281  mpfrcl  20794  cpmatelimp  21358  cpmatelimp2  21360  f1o3d  30430  oddpwdc  31788  altopthsn  33682  bj-animbi  34158  volsupnfl  35253  mbfresfi  35254  qirropth  40020  brcofffn  40905  lighneal  44297
 Copyright terms: Public domain W3C validator