Theorem 3jca 604

Description: Join consequents with conjunction.

Hypotheses

Ref	Expression
3jca.1	|- (ph -> ps)
3jca.2	|- (ph -> ch)
3jca.3	|- (ph -> th)

Assertion

Ref	Expression
3jca	|- (ph -> (ps /\ ch /\ th))

Proof of Theorem 3jca

Step	Hyp	Ref	Expression
1		3jca.1	. . . 4 |- (ph -> ps)
2		3jca.2	. . . 4 |- (ph -> ch)
3	1, 2	jca 236	. . 3 |- (ph -> (ps /\ ch))
4		3jca.3	. . 3 |- (ph -> th)
5	3, 4	jca 236	. 2 |- (ph -> ((ps /\ ch) /\ th))
6		df-3an 583	. 2 |- ((ps /\ ch /\ th) <-> ((ps /\ ch) /\ th))
7	5, 6	sylibr 175	1 |- (ph -> (ps /\ ch /\ th))

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  syl3anc 629  tpss 1855  ordelord 2221  tz7.49 2997  ltexpq 3874  divdivdivt 4265  divdiv23t 4271  le2tri3 4311  ltdivmult 4408  qrecclt 4646  osumlem3 5532  pjclem4 5653  pj3s 5659  stle 5681  stadd3 5689  atexch 5769  atcvatlem 5770  atcvat4 5775

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org