Theorem jcad 305

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 138	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 66	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  jca2  306  jctild  314  jctird  315  ancld  323  ancrd  324  anim12ii  341  equsex  1721  equsexd  1722  rexim  2564  rr19.28v  2870  sotricim  4306  sotritrieq  4308  ordsucss  4486  ordpwsucss  4549  peano5  4580  iss  4935  funssres  5238  ssimaex  5555  elpreima  5613  resflem  5658  tposfo2  6244  nnmord  6494  map0g  6664  mapsn  6666  enq0tr  7389  addnqprl  7484  addnqpru  7485  cauappcvgprlemdisj  7606  lttri3  7992  ltleap  8544  mulgt1  8772  nominpos  9108  uzind  9316  indstr  9545  eqreznegel  9566  shftuz  10774  caucvgrelemcau  10937  sqrtsq  11001  mulcn2  11268  dvdsgcdb  11961  algcvgblem  11996  lcmdvdsb  12031  rpexp  12100  infpnlem1  12304  cnntr  12984  cnrest2  12995  txlm  13038  metrest  13265  bj-om  13937