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 2941  oneqmini 3023  oneqmin 3024  asymref2 3446  funss 3540  funssres 3558  ssimaex 3774  eqfnfv 3803  cbvfo 3891  isomin 3905  oaordex 4198  oa00 4199  oarec 4202  odi 4216  oneo 4218  oeordsuc 4227  oelim2 4228  nnarcl 4238  nnaordex 4255  nnawordex 4256  eceqopreq 4319  mapsn 4351  sbthbg 4464  sdomdomtr 4475  onomeneq 4525  pssnn 4544  unfilem1 4560  inf0 4615  inf3lem3 4624  inf3lem4 4625  cplem1 4730  karden 4736  aceq5lem5 4749  zorn2lem4 4801  zorn2lem6 4803  zorn2lem7 4804  fodomb 4810  unidom 4818  carden 4841  sucdom 4852  sucdomOLD 4853  alephordi 4885  cardinfima 4902  alephval3 4914  indpi 5046  genpcl 5123  addclprlem2 5131  ltaddpr 5152  ltexprlem5 5158  suplem1pr 5173  suppsr2 5235  ltlent 5534  mulgt1t 5847  xrmaxltt 5915  xrltmint 5916  maxlet 5920  lemint 5923  maxltt 5924  nominpos 6045  sup2 6053  infmrcl 6071  supxrre 6085  uzind 6207  iooval2t 6368  elioc2t 6391  elico2t 6392  elicc2t 6393  ioojoint 6417  elfzlem 6474  fzoptht 6503  cvg3 6923  cvganz 6924  fsumcom 7028  clm3 7079  clim2serzt 7134  iserzmulc1 7136  caucvg 7163  serzf0 7169  ser1f0 7170  expcnvlem6 7232  ivthlem7 7287  infpnlem1 7507  infxpidmlem10 7562  clsval2 7682  sncld 7784  opnuni 7865  opnin 7866  metcnss 7895  xplmi 7970  bcthlem14 8009  ubthlem6 8530  ococss 9161  chocuni 9167  occllem6 9173  0cnop 9898  0cnfn 9899  nmopunt 9934  stm1add 10167  stm1add3 10169  mdsl1 10243  chrelat2 10287  atexcht 10303  atcvat4 10319  mdsymlem3 10327  mrdmcd 10693  cmphmia 10697  cmphmib 10698  ismonc 10713

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