Theorem jcad 531

Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 15-Jul-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 445	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 64	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 369

This theorem is referenced by:  jctild  541  jctird  542  ancld  551  ancrd  552  anim12ii  568  oplem1  962  2eu1  2307  rr19.28v  3167  disjxiun  4364  oneqmini  4843  iss  5233  funssres  5536  ssimaex  5839  elpreima  5909  isomin  6134  oneqmin  6539  frxp  6809  tposfo2  6896  onfununi  6930  oaordex  7125  oa00  7126  odi  7146  oneo  7148  oeordsuc  7161  oelim2  7162  nnarcl  7183  nnmord  7199  nnneo  7218  map0g  7377  mapsn  7379  domtriord  7582  onomeneq  7626  pssnn  7654  findcard3  7678  unfilem1  7699  fodomfib  7715  inf0  7952  inf3lem3  7961  inf3lem4  7962  tcel  8089  cplem1  8220  karden  8226  fidomtri2  8288  alephordi  8368  cardinfima  8391  alephval3  8404  dfac5lem5  8421  isf34lem4  8670  axcc4  8732  axdc3lem2  8744  zorn2lem4  8792  zorn2lem6  8794  zorn2lem7  8795  fodomb  8817  indpi  9196  genpcl  9297  addclprlem2  9306  ltaddpr  9323  ltexprlem5  9329  suplem1pr  9341  ltlen  9597  dedekind  9655  mulgt1  10318  sup2  10415  infmrcl  10438  nominpos  10692  uzind  10871  eqreznegel  11086  xrmaxlt  11303  xrltmin  11304  xrmaxle  11305  xrlemin  11306  xmullem2  11378  ccatopth  12606  shftuz  12904  sqreulem  13194  limsupbnd2  13308  mulcn2  13420  sadcaddlem  14109  dvdsgcdb  14184  algcvgblem  14208  rpexp  14263  iserodd  14361  infpnlem1  14430  divsfval  14954  iscatd  15080  posasymb  15699  plttr  15717  joinle  15761  meetle  15775  latnlej  15815  latnlej2  15818  lsmlub  16800  imasring  17381  unitmulclb  17427  lbspss  17841  lspsneu  17882  lspprat  17912  assapropd  18089  isclo2  19675  cncls2  19860  cncls  19861  cnntr  19862  cnrest2  19873  cmpsub  19986  cmpcld  19988  kgenss  20129  ptpjpre1  20157  txcn  20212  txlm  20234  qtoptop2  20285  cmphaushmeo  20386  fbun  20426  isfild  20444  ssfg  20458  fbasrn  20470  fgtr  20476  ufinffr  20515  rnelfm  20539  fmfnfmlem4  20543  fclsnei  20605  ghmcnp  20698  metrest  21112  icoopnst  21524  iocopnst  21525  dgreq0  22747  plyexmo  22794  cxpeq0  23146  mumullem2  23571  chpchtsum  23611  bposlem7  23682  lgsqr  23738  usg2wlkeq  24829  usg2spthonot0  25010  ex-natded5.3-2  25250  ubthlem1  25903  axhcompl-zf  26032  ococss  26328  nmopun  27049  elpjrn  27225  stm1addi  27280  stm1add3i  27282  mdsl1i  27356  chrelat2i  27400  atexch  27416  atcvat4i  27432  mdsymlem3  27440  bian1d  27483  eldmgm  28753  subfacval2  28820  cvmlift2lem10  28946  climuzcnv  29226  fundmpss  29362  preddowncl  29441  soseq  29499  sltres  29589  segconeq  29813  ifscgr  29847  endofsegid  29888  colinbtwnle  29921  onsuct0  30059  trer  30300  ivthALT  30319  fnessref  30341  fnemeet2  30351  fnejoin2  30353  isbnd2  30445  bfplem2  30485  ghomco  30511  cnf1dd  30656  contrd  30663  mpt2bi123f  30737  mptbi12f  30741  jca2  30751  jca2r  30752  prter2  30788  lcmdvdsb  31385  pm11.71  31471  bnj600  34324  bj-finsumval0  35010  bj-bary1  35025  lshpset2N  35257  cvrnbtwn2  35413  cvrnbtwn3  35414  cvrnbtwn4  35417  cvlcvr1  35477  hlrelat2  35540  cvrat4  35580  islpln2a  35685  linepsubN  35889  elpaddn0  35937  paddssw2  35981  pmapjoin  35989  ispsubcl2N  36084  dochkrshp  37526  dochsatshp  37591  mapdh9a  37930  hdmap11lem2  37985  pwinfi3  38177