Theorem jcad 307

Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem jcad

Step	Hyp	Ref	Expression
1		jcad.1	. 2 |- ( ph -> ( ps -> ch ) )
2		jcad.2	. 2 |- ( ph -> ( ps -> th ) )
3		pm3.2 139	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 66	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1752  equsexd  1753  rexim  2602  rr19.28v  2920  sotricim  4388  sotritrieq  4390  ordsucss  4570  ordpwsucss  4633  peano5  4664  iss  5024  funssres  5332  ssimaex  5663  elpreima  5722  resflem  5767  tposfo2  6376  nnmord  6626  map0g  6798  mapsn  6800  enq0tr  7582  addnqprl  7677  addnqpru  7678  cauappcvgprlemdisj  7799  lttri3  8187  ltleap  8740  mulgt1  8971  nominpos  9310  uzind  9519  indstr  9749  eqreznegel  9770  ccatopth  11207  shftuz  11243  caucvgrelemcau  11406  sqrtsq  11470  mulcn2  11738  dvdsgcdb  12449  algcvgblem  12486  lcmdvdsb  12521  rpexp  12590  infpnlem1  12797  imasring  13941  unitmulclb  13991  cnntr  14812  cnrest2  14823  txlm  14866  metrest  15093  bj-om  16072