Theorem jcad 535

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 448	. 2 |- ( ch -> ( th -> ( ch /\ th ) ) )
4	1, 2, 3	syl6c 66	1 |- ( ph -> ( ps -> ( ch /\ th ) ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  jctild  545  jctird  546  ancld  555  ancrd  556  anim12ii  572  oplem1  972  2eu1  2354  rr19.28v  3220  disjxiun  4423  iss  5172  preddowncl  5426  oneqmini  5493  funssres  5641  ssimaex  5946  elpreima  6017  isomin  6243  oneqmin  6646  frxp  6917  tposfo2  7004  onfununi  7068  oaordex  7267  oa00  7268  odi  7288  oneo  7290  oeordsuc  7303  oelim2  7304  nnarcl  7325  nnmord  7341  nnneo  7360  map0g  7519  mapsn  7521  domtriord  7724  onomeneq  7768  pssnn  7796  findcard3  7820  unfilem1  7841  fodomfib  7857  inf0  8126  inf3lem3  8135  inf3lem4  8136  tcel  8228  cplem1  8359  karden  8365  fidomtri2  8427  alephordi  8503  cardinfima  8526  alephval3  8539  dfac5lem5  8556  isf34lem4  8805  axcc4  8867  axdc3lem2  8879  zorn2lem4  8927  zorn2lem6  8929  zorn2lem7  8930  fodomb  8952  indpi  9331  genpcl  9432  addclprlem2  9441  ltaddpr  9458  ltexprlem5  9464  suplem1pr  9476  ltlen  9734  dedekind  9796  mulgt1  10463  sup2  10565  infmrclOLD  10593  nominpos  10849  uzind  11027  eqreznegel  11249  xrmaxlt  11476  xrltmin  11477  xrmaxle  11478  xrlemin  11479  xmullem2  11551  ccatopth  12811  shftuz  13111  sqreulem  13401  limsupbnd2  13524  limsupbnd2OLD  13525  mulcn2  13637  sadcaddlem  14405  dvdsgcdb  14483  algcvgblem  14507  lcmdvdsb  14549  rpexp  14643  iserodd  14748  infpnlem1  14817  divsfval  15404  iscatd  15530  posasymb  16149  plttr  16167  joinle  16211  meetle  16225  latnlej  16265  latnlej2  16268  lsmlub  17250  imasring  17782  unitmulclb  17828  lbspss  18240  lspsneu  18281  lspprat  18311  assapropd  18486  isclo2  20035  cncls2  20220  cncls  20221  cnntr  20222  cnrest2  20233  cmpsub  20346  cmpcld  20348  kgenss  20489  ptpjpre1  20517  txcn  20572  txlm  20594  qtoptop2  20645  cmphaushmeo  20746  fbun  20786  isfild  20804  ssfg  20818  fbasrn  20830  fgtr  20836  ufinffr  20875  rnelfm  20899  fmfnfmlem4  20903  fclsnei  20965  ghmcnp  21060  metrest  21470  icoopnst  21863  iocopnst  21864  dgreq0  23087  plyexmo  23134  cxpeq0  23488  eldmgm  23812  mumullem2  23970  chpchtsum  24010  bposlem7  24081  lgsqr  24137  usg2wlkeq  25281  usg2spthonot0  25462  ex-natded5.3-2  25703  ubthlem1  26357  axhcompl-zf  26486  ococss  26781  nmopun  27502  elpjrn  27678  stm1addi  27733  stm1add3i  27735  mdsl1i  27809  chrelat2i  27853  atexch  27869  atcvat4i  27885  mdsymlem3  27893  bian1d  27935  bnj600  29518  subfacval2  29698  cvmlift2lem10  29823  climuzcnv  30103  fundmpss  30194  soseq  30279  sltres  30338  segconeq  30562  ifscgr  30596  endofsegid  30637  colinbtwnle  30670  trer  30757  ivthALT  30776  fnessref  30798  fnemeet2  30808  fnejoin2  30810  onsuct0  30886  bj-finsumval0  31447  bj-bary1  31462  icorempt2  31488  isbasisrelowllem1  31492  isbasisrelowllem2  31493  relowlpssretop  31501  poimirlem31  31675  isbnd2  31819  bfplem2  31859  ghomco  31885  cnf1dd  32030  contrd  32037  mpt2bi123f  32110  mptbi12f  32114  jca2  32124  jca2r  32125  prter2  32161  lshpset2N  32394  cvrnbtwn2  32550  cvrnbtwn3  32551  cvrnbtwn4  32554  cvlcvr1  32614  hlrelat2  32677  cvrat4  32717  islpln2a  32822  linepsubN  33026  elpaddn0  33074  paddssw2  33118  pmapjoin  33126  ispsubcl2N  33221  dochkrshp  34663  dochsatshp  34728  mapdh9a  35067  hdmap11lem2  35122  pwinfi3  35866  pm11.71  36384  sgoldbaltlem2  38271