Theorem jcai 559

Description: Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
jcai.1	|- ( ph -> ps )
jcai.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
jcai	|- ( ph -> ( ps /\ ch ) )

Proof of Theorem jcai

Step	Hyp	Ref	Expression
1		jcai.1	. 2 |- ( ph -> ps )
2		jcai.2	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	mpd 15	. 2 |- ( ph -> ch )
4	1, 3	jca 554	1 |- ( ph -> ( ps /\ ch ) )

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  2530  reu6  3395  f1ocnv2d  6886  onfin2  8152  nnoddn2prm  15516  isinitoi  16653  istermoi  16654  iszeroi  16659  mpfrcl  19518  cpmatelimp  20517  cpmatelimp2  20519  clwlksf1clwwlklem  26968  f1o3d  29431  oddpwdc  30416  altopthsn  32068  volsupnfl  33454  mbfresfi  33456  qirropth  37473  brcofffn  38329  lighneal  41528