Theorem jcai 543

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  euan  2369  reu6  3238  f1ocnv2d  6546  onfin2  7789  isinitoi  15946  istermoi  15947  iszeroi  15952  mpfrcl  18789  cpmatelimp  19784  cpmatelimp2  19786  clwlkf1clwwlklem  25625  f1o3d  28277  oddpwdc  29235  altopthsn  30776  volsupnfl  32029  mbfresfi  32031  qirropth  35800