Theorem jcad 603

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  jctild 604  jctird 605  pm5.21nd 684  pm5.75 754  oplem1 777  euor2 1477  oneqmini 3024  dfwe2 3140  oneqmin 3162  asymref2 3532  funss 3639  funssres 3657  ssimaex 3879  eqfnfv 3909  cbvfo 3999  isomin 4013  onfununi 4209  oaordex 4328  oa00 4329  oarec 4332  odi 4346  oneo 4348  oeordsuc 4357  oelim2 4358  nnarcl 4372  nnaordex 4389  nnawordex 4390  eceqopreq 4454  mapsn 4486  sbthbg 4603  sdomdomtr 4614  onomeneq 4665  pssnn 4681  unfilem1 4694  fodomfib 4710  inf0 4751  inf3lem3 4760  inf3lem4 4761  cplem1 4866  karden 4872  aceq5lem5 4885  zorn2lem4 4937  zorn2lem6 4939  zorn2lem7 4940  fodomb 4946  unidom 4954  carden 4979  sucdom 4992  alephordi 5024  cardinfima 5041  alephval3 5053  indpi 5188  genpcl 5265  addclprlem2 5273  ltaddpr 5294  ltexprlem5 5300  suplem1pr 5315  suppsr2 5377  ltlen 5676  mulgt1 5989  xrmaxlt 6058  xrltmin 6059  maxle 6063  lemin 6066  maxlt 6067  nominpos 6189  sup2 6219  infmrcl 6237  supxrre 6251  uzind 6376  iooval2 6493  elioc2 6516  elico2 6517  elicc2 6518  ioojoin 6543  elfzlem 6601  fzopth 6632  cvg3i 7126  cvganz 7127  fsumcom 7231  clm3i 7282  clim2serz 7337  iserzmulc1 7339  caucvgi 7366  serzf0i 7372  expcnvlem6 7436  explecnv 7438  ivthlem7 7492  infpnlem1 7718  infxpidmlem10 7773  clsval2 7895  sncld 7997  opnuni 8078  opnin 8079  metequiv 8091  metcnss 8109  xplmi 8184  bcthlem14 8223  ubthlem6 8792  ococss 9442  chocunii 9448  occllem6 9454  0cnop 10182  0cnfn 10183  nmopun 10218  stm1addi 10453  stm1add3i 10455  mdsl1i 10529  chrelat2i 10573  atexch 10590  atcvat4i 10606  mdsymlem3 10614  mrdmcd 11249  cmphmia 11253  cmphmib 11254  ismonc 11269  isepic 11279  dmsdtriord 11408  trer 11409  ordtypelem4 11430  ordtypelem7 11433  onsdom 11437  elomsubsd 11446  omsublim 11448  subcld 11480  cnsubsp2 11484  compsub 11488  cptclsscpt 11489  hscptsscld 11491  cnconn 11503  subtopmetlem 11505  subtopmet 11506  reconnlem5 11511  ivthALT 11515  fnessref 11564  neibastop1 11579  neibastop2 11584  fgfil 11638  fbfgss 11640  filrn 11643  isufil2 11650  ufilen 11664  rnelfm 11699  fmfnfmlem4 11703  fmfnfm 11704  filnetlem5 11767  filnet 11768  gapmlem 11783  gapm 11784  elpreima 11792  fipreima 11848  blssp 11908  blhalf 11911  caushft 11916  icoopnst 11940  iocopnst 11941  cnss 11953  lmtlm 11969  txcn 11979  txcld 11985  sstotbnd 11992  totbndss 11993  isbnd3 11997  ismtyres 12010  heiborlem13 12023  heiborlem28 12038  heiborlem35 12045  recms 12066

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 145  df-an 223

Copyright terms: Public domain