Theorem jcai 313

Description: Deduction replacing implication with conjunction.

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 29	. 2 |- (ph -> ch)
4	1, 3	jca 310	1 |- (ph -> (ps /\ ch))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  reu6 2443  opth 3532  en3d 5460  ac6sfilem3 5508  ordtypelem7 5690  hartog 5693  omsubsuc2 5878  gapm 9462  hausfillim 10303  iintlem1 15010  iint 15012  ordtypelem7OLD 15381  hartogOLD 15384  omsubsuc2OLD 15387  supfil 15560  filssufillem 15570  ufilen 15579  ufcondr 15581  rnelfm 15593  fmfnfm 15598  tailmap 15636  filnet 15645  sdc 15811

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain