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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1780  equsexd  1782  rexim  2644  rr19.28v  2966  sotricim  4468  sotritrieq  4470  ordsucss  4651  ordpwsucss  4714  peano5  4745  iss  5109  funssres  5420  ssimaex  5764  elpreima  5828  resflem  5872  tposfo2  6538  nnmord  6790  map0g  6969  mapsn  6972  enq0tr  7801  addnqprl  7896  addnqpru  7897  cauappcvgprlemdisj  8018  lttri3  8405  ltleap  8962  mulgt1  9195  nominpos  9547  uzind  9761  indstr  10002  eqreznegel  10023  ccatopth  11502  shftuz  11596  caucvgrelemcau  11760  sqrtsq  11824  mulcn2  12094  dvdsgcdb  12806  algcvgblem  12843  lcmdvdsb  12878  rpexp  12948  infpnlem1  13158  imasring  14418  unitmulclb  14470  assapropd  15063  cnntr  15375  cnrest2  15386  txlm  15429  metrest  15656  uspgr2wlkeq  16704  bj-om  17061