Theorem jcad 533

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

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  jctild  543  jctird  544  ancld  553  ancrd  554  anim12ii  570  oplem1  955  2eu1  2364  rr19.28v  3102  disjxiun  4289  oneqmini  4770  iss  5154  funssres  5458  ssimaex  5756  elpreima  5823  isomin  6028  oneqmin  6416  frxp  6682  tposfo2  6768  onfununi  6802  oaordex  6997  oa00  6998  odi  7018  oneo  7020  oeordsuc  7033  oelim2  7034  nnarcl  7055  nnmord  7071  nnneo  7090  map0g  7252  mapsn  7254  domtriord  7457  onomeneq  7500  pssnn  7531  findcard3  7555  unfilem1  7576  fodomfib  7591  inf0  7827  inf3lem3  7836  inf3lem4  7837  tcel  7965  cplem1  8096  karden  8102  fidomtri2  8164  alephordi  8244  cardinfima  8267  alephval3  8280  dfac5lem5  8297  isf34lem4  8546  axcc4  8608  axdc3lem2  8620  zorn2lem4  8668  zorn2lem6  8670  zorn2lem7  8671  fodomb  8693  indpi  9076  genpcl  9177  addclprlem2  9186  ltaddpr  9203  ltexprlem5  9209  suplem1pr  9221  ltlen  9476  dedekind  9533  mulgt1  10188  sup2  10286  infmrcl  10309  nominpos  10561  uzind  10733  eqreznegel  10940  xrmaxlt  11153  xrltmin  11154  xrmaxle  11155  xrlemin  11156  xmullem2  11228  ccatopth  12364  shftuz  12558  sqreulem  12847  limsupbnd2  12961  mulcn2  13073  sadcaddlem  13653  dvdsgcdb  13728  algcvgblem  13752  rpexp  13806  iserodd  13902  infpnlem1  13971  divsfval  14485  iscatd  14611  posasymb  15122  plttr  15140  joinle  15184  meetle  15198  latnlej  15238  latnlej2  15241  lsmlub  16162  imasrng  16711  unitmulclb  16757  lbspss  17163  lspsneu  17204  lspprat  17234  assapropd  17398  isclo2  18692  cncls2  18877  cncls  18878  cnntr  18879  cnrest2  18890  cmpsub  19003  cmpcld  19005  kgenss  19116  ptpjpre1  19144  txcn  19199  txlm  19221  qtoptop2  19272  cmphaushmeo  19373  fbun  19413  isfild  19431  ssfg  19445  fbasrn  19457  fgtr  19463  ufinffr  19502  rnelfm  19526  fmfnfmlem4  19530  fclsnei  19592  ghmcnp  19685  metrest  20099  icoopnst  20511  iocopnst  20512  dgreq0  21732  plyexmo  21779  cxpeq0  22123  mumullem2  22518  chpchtsum  22558  bposlem7  22629  lgsqr  22685  ex-natded5.3-2  23615  ubthlem1  24271  axhcompl-zf  24400  ococss  24696  nmopun  25418  elpjrn  25594  stm1addi  25649  stm1add3i  25651  mdsl1i  25725  chrelat2i  25769  atexch  25785  atcvat4i  25801  mdsymlem3  25809  bian1d  25851  eldmgm  27008  subfacval2  27075  cvmlift2lem10  27201  climuzcnv  27316  fundmpss  27577  preddowncl  27657  soseq  27715  sltres  27805  segconeq  28041  ifscgr  28075  endofsegid  28116  colinbtwnle  28149  onsuct0  28287  trer  28511  ivthALT  28530  fnessref  28565  fnemeet2  28588  fnejoin2  28590  isbnd2  28682  bfplem2  28722  ghomco  28748  cnf1dd  28893  contrd  28900  mpt2bi123f  28975  mptbi12f  28979  jca2  28989  jca2r  28990  prter2  29026  pm11.71  29650  usg2wlkeq  30289  usg2spthonot0  30408  bnj600  31912  bj-finsumval0  32583  bj-bary1  32601  lshpset2N  32764  cvrnbtwn2  32920  cvrnbtwn3  32921  cvrnbtwn4  32924  cvlcvr1  32984  hlrelat2  33047  cvrat4  33087  islpln2a  33192  linepsubN  33396  elpaddn0  33444  paddssw2  33488  pmapjoin  33496  ispsubcl2N  33591  dochkrshp  35031  dochsatshp  35096  mapdh9a  35435  hdmap11lem2  35490