Theorem jcad 599

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 600  jctird 601  pm5.21nd 679  pm5.75 748  oplem1 771  euor2 1435  dfwe2 2930  oneqmini 3012  oneqmin 3013  asymref2 3432  funss 3526  funssres 3544  ssimaex 3759  eqfnfv 3788  cbvfo 3876  isomin 3890  oaordex 4182  oa00 4183  oarec 4186  odi 4200  oneo 4202  oeordsuc 4211  oelim2 4212  nnarcl 4222  nnaordex 4239  nnawordex 4240  eceqopreq 4303  mapsn 4335  sbthbg 4444  sdomdomtr 4455  onomeneq 4504  pssnn 4519  unfilem1 4530  fodomfib 4547  inf0 4586  inf3lem3 4595  inf3lem4 4596  cplem1 4700  karden 4706  aceq5lem5 4719  zorn2lem4 4771  zorn2lem6 4773  zorn2lem7 4774  fodomb 4780  unidom 4788  carden 4811  sucdom 4822  alephordi 4854  cardinfima 4871  alephval3 4883  indpi 5014  genpcl 5091  addclprlem2 5099  ltaddpr 5120  ltexprlem5 5126  suplem1pr 5141  suppsr2 5203  ltlent 5503  mulgt1t 5809  xrmaxltt 5869  xrltmint 5870  maxlet 5874  lemint 5877  maxltt 5878  nominpos 5998  sup2 6006  infmrcl 6024  supxrre 6038  uzind 6161  iooval2t 6312  elioc2t 6330  elico2t 6331  elicc2t 6332  elfzlem 6413  fzoptht 6442  cvg3 6868  cvganz 6869  fsumcom 6974  clm3 7025  clim2serzt 7078  iserzmulc1 7080  caucvg 7107  serzf0 7113  ser1f0 7114  expcnvlem6 7175  ivthlem7 7230  ivthlem7OLD 7239  infpnlem1 7457  infxpidmlem10 7512  clsval2 7635  sncld 7737  opnuni 7820  opnin 7821  metcnss 7850  xplmi 7923  bcthlem14 7962  ubthlem6 8478  ococss 9105  chocuni 9111  occllem6 9117  0cnop 9842  0cnfn 9843  nmopunt 9877  stm1add 10110  stm1add3 10112  mdsl1 10185  chrelat2 10229  atexcht 10245  atcvat4 10261  mdsymlem3 10269  mrdmcd 10602  cmphmia 10606  cmphmib 10607  ismonc 10620

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