Theorem jcai 534

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 530	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 367

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 185  df-an 369

This theorem is referenced by:  euan  2348  reu6  3285  f1ocnv2d  6499  onfin2  7702  isinitoi  15481  istermoi  15482  iszeroi  15487  mpfrcl  18382  cpmatelimp  19380  cpmatelimp2  19382  clwlkf1clwwlklem  25051  f1o3d  27690  oddpwdc  28557  altopthsn  29839  volsupnfl  30299  mbfresfi  30301  qirropth  31083