Theorem jcad 602

Description: Deduction conjoining the consequents of two implications.

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	. . . 4 |- (ph -> (ps -> ch))
2	1	imp 350	. . 3 |- ((ph /\ ps) -> ch)
3		jcad.2	. . . 4 |- (ph -> (ps -> th))
4	3	imp 350	. . 3 |- ((ph /\ ps) -> th)
5	2, 4	jca 288	. 2 |- ((ph /\ ps) -> (ch /\ th))
6	5	ex 373	1 |- (ph -> (ps -> (ch /\ th)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  jctild 603  jctird 604  pm5.21nd 682  pm5.75 751  oplem1 774  euor2 1440  dfwe2 2942  oneqmini 3024  oneqmin 3025  asymref2 3447  funss 3541  funssres 3559  ssimaex 3775  eqfnfv 3804  cbvfo 3892  isomin 3906  oaordex 4199  oa00 4200  oarec 4203  odi 4217  oneo 4219  oeordsuc 4228  oelim2 4229  nnarcl 4239  nnaordex 4256  nnawordex 4257  eceqopreq 4320  mapsn 4352  sbthbg 4465  sdomdomtr 4476  onomeneq 4526  pssnn 4546  unfilem1 4562  inf0 4622  inf3lem3 4631  inf3lem4 4632  cplem1 4737  karden 4743  aceq5lem5 4756  zorn2lem4 4808  zorn2lem6 4810  zorn2lem7 4811  fodomb 4817  unidom 4825  carden 4848  sucdom 4859  sucdomOLD 4860  alephordi 4892  cardinfima 4909  alephval3 4921  indpi 5053  genpcl 5130  addclprlem2 5138  ltaddpr 5159  ltexprlem5 5165  suplem1pr 5180  suppsr2 5242  ltlent 5541  mulgt1t 5854  xrmaxltt 5922  xrltmint 5923  maxlet 5927  lemint 5930  maxltt 5931  nominpos 6052  sup2 6060  infmrcl 6078  supxrre 6092  uzind 6214  iooval2t 6375  elioc2t 6398  elico2t 6399  elicc2t 6400  ioojoint 6424  elfzlem 6481  fzoptht 6510  cvg3 6930  cvganz 6931  fsumcom 7035  clm3 7086  clim2serzt 7141  iserzmulc1 7143  caucvg 7170  serzf0 7176  ser1f0 7177  expcnvlem6 7239  ivthlem7 7294  infpnlem1 7514  infxpidmlem10 7569  clsval2 7689  sncld 7791  opnuni 7872  opnin 7873  metcnss 7902  xplmi 7977  bcthlem14 8016  ubthlem6 8537  ococss 9168  chocuni 9174  occllem6 9180  0cnop 9905  0cnfn 9906  nmopunt 9941  stm1add 10175  stm1add3 10177  mdsl1 10251  chrelat2 10295  atexcht 10311  atcvat4 10327  mdsymlem3 10335  mrdmcd 10701  cmphmia 10705  cmphmib 10706  ismonc 10721

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 147  df-an 225

Copyright terms: Public domain