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  3151  disjxiun  4358  iss  5109  preddowncl  5364  oneqmini  5431  funssres  5579  ssimaex  5885  elpreima  5956  isomin  6182  oneqmin  6585  frxp  6856  tposfo2  6946  onfununi  7010  oaordex  7209  oa00  7210  odi  7230  oneo  7232  oeordsuc  7245  oelim2  7246  nnarcl  7267  nnmord  7283  nnneo  7302  map0g  7461  mapsn  7463  domtriord  7666  onomeneq  7710  pssnn  7738  findcard3  7762  unfilem1  7783  fodomfib  7799  inf0  8074  inf3lem3  8083  inf3lem4  8084  tcel  8176  cplem1  8307  karden  8313  fidomtri2  8375  alephordi  8451  cardinfima  8474  alephval3  8487  dfac5lem5  8504  isf34lem4  8753  axcc4  8815  axdc3lem2  8827  zorn2lem4  8875  zorn2lem6  8877  zorn2lem7  8878  fodomb  8900  indpi  9278  genpcl  9379  addclprlem2  9388  ltaddpr  9405  ltexprlem5  9411  suplem1pr  9423  ltlen  9681  dedekind  9743  mulgt1  10410  sup2  10511  infmrclOLD  10539  nominpos  10795  uzind  10973  eqreznegel  11195  xrmaxlt  11422  xrltmin  11423  xrmaxle  11424  xrlemin  11425  xmullem2  11497  ccatopth  12767  shftuz  13071  sqreulem  13361  limsupbnd2  13484  limsupbnd2OLD  13485  mulcn2  13597  sadcaddlem  14369  dvdsgcdb  14450  algcvgblem  14474  lcmdvdsb  14516  rpexp  14610  iserodd  14723  infpnlem1  14792  divsfval  15391  iscatd  15517  posasymb  16136  plttr  16154  joinle  16198  meetle  16212  latnlej  16252  latnlej2  16255  lsmlub  17253  imasring  17785  unitmulclb  17831  lbspss  18243  lspsneu  18284  lspprat  18314  assapropd  18489  isclo2  20041  cncls2  20226  cncls  20227  cnntr  20228  cnrest2  20239  cmpsub  20352  cmpcld  20354  kgenss  20495  ptpjpre1  20523  txcn  20578  txlm  20600  qtoptop2  20651  cmphaushmeo  20752  fbun  20792  isfild  20810  ssfg  20824  fbasrn  20836  fgtr  20842  ufinffr  20881  rnelfm  20905  fmfnfmlem4  20909  fclsnei  20971  ghmcnp  21066  metrest  21476  icoopnst  21904  iocopnst  21905  dgreq0  23156  plyexmo  23203  cxpeq0  23560  eldmgm  23884  mumullem2  24044  chpchtsum  24084  bposlem7  24155  lgsqr  24211  usg2wlkeq  25373  usg2spthonot0  25554  ex-natded5.3-2  25795  ubthlem1  26449  axhcompl-zf  26588  ococss  26883  nmopun  27604  elpjrn  27780  stm1addi  27835  stm1add3i  27837  mdsl1i  27911  chrelat2i  27955  atexch  27971  atcvat4i  27987  mdsymlem3  27995  bian1d  28037  bnj600  29677  subfacval2  29857  cvmlift2lem10  29982  climuzcnv  30262  fundmpss  30353  soseq  30438  sltres  30497  segconeq  30721  ifscgr  30755  endofsegid  30796  colinbtwnle  30829  trer  30916  ivthALT  30935  fnessref  30957  fnemeet2  30967  fnejoin2  30969  onsuct0  31045  bj-finsumval0  31609  bj-bary1  31624  icorempt2  31661  isbasisrelowllem1  31665  isbasisrelowllem2  31666  relowlpssretop  31674  finxpsuclem  31696  poimirlem31  31878  isbnd2  32022  bfplem2  32062  ghomco  32088  cnf1dd  32233  contrd  32240  mpt2bi123f  32313  mptbi12f  32317  jca2  32327  jca2r  32328  prter2  32364  lshpset2N  32597  cvrnbtwn2  32753  cvrnbtwn3  32754  cvrnbtwn4  32757  cvlcvr1  32817  hlrelat2  32880  cvrat4  32920  islpln2a  33025  linepsubN  33229  elpaddn0  33277  paddssw2  33321  pmapjoin  33329  ispsubcl2N  33424  dochkrshp  34866  dochsatshp  34931  mapdh9a  35270  hdmap11lem2  35325  pwinfi3  36080  pm11.71  36660  sgoldbaltlem2  38694