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  962  2eu1  2386  rr19.28v  3246  disjxiun  4444  oneqmini  4929  iss  5321  funssres  5628  ssimaex  5932  elpreima  6001  isomin  6221  oneqmin  6624  frxp  6893  tposfo2  6978  onfununi  7012  oaordex  7207  oa00  7208  odi  7228  oneo  7230  oeordsuc  7243  oelim2  7244  nnarcl  7265  nnmord  7281  nnneo  7300  map0g  7458  mapsn  7460  domtriord  7663  onomeneq  7707  pssnn  7738  findcard3  7763  unfilem1  7784  fodomfib  7800  inf0  8038  inf3lem3  8047  inf3lem4  8048  tcel  8176  cplem1  8307  karden  8313  fidomtri2  8375  alephordi  8455  cardinfima  8478  alephval3  8491  dfac5lem5  8508  isf34lem4  8757  axcc4  8819  axdc3lem2  8831  zorn2lem4  8879  zorn2lem6  8881  zorn2lem7  8882  fodomb  8904  indpi  9285  genpcl  9386  addclprlem2  9395  ltaddpr  9412  ltexprlem5  9418  suplem1pr  9430  ltlen  9686  dedekind  9743  mulgt1  10401  sup2  10499  infmrcl  10522  nominpos  10775  uzind  10952  eqreznegel  11167  xrmaxlt  11382  xrltmin  11383  xrmaxle  11384  xrlemin  11385  xmullem2  11457  ccatopth  12658  shftuz  12865  sqreulem  13155  limsupbnd2  13269  mulcn2  13381  sadcaddlem  13966  dvdsgcdb  14041  algcvgblem  14065  rpexp  14120  iserodd  14218  infpnlem1  14287  divsfval  14802  iscatd  14928  posasymb  15439  plttr  15457  joinle  15501  meetle  15515  latnlej  15555  latnlej2  15558  lsmlub  16489  imasrng  17069  unitmulclb  17115  lbspss  17528  lspsneu  17569  lspprat  17599  assapropd  17775  isclo2  19383  cncls2  19568  cncls  19569  cnntr  19570  cnrest2  19581  cmpsub  19694  cmpcld  19696  kgenss  19807  ptpjpre1  19835  txcn  19890  txlm  19912  qtoptop2  19963  cmphaushmeo  20064  fbun  20104  isfild  20122  ssfg  20136  fbasrn  20148  fgtr  20154  ufinffr  20193  rnelfm  20217  fmfnfmlem4  20221  fclsnei  20283  ghmcnp  20376  metrest  20790  icoopnst  21202  iocopnst  21203  dgreq0  22424  plyexmo  22471  cxpeq0  22815  mumullem2  23210  chpchtsum  23250  bposlem7  23321  lgsqr  23377  usg2wlkeq  24412  usg2spthonot0  24593  ex-natded5.3-2  24834  ubthlem1  25490  axhcompl-zf  25619  ococss  25915  nmopun  26637  elpjrn  26813  stm1addi  26868  stm1add3i  26870  mdsl1i  26944  chrelat2i  26988  atexch  27004  atcvat4i  27020  mdsymlem3  27028  bian1d  27070  eldmgm  28232  subfacval2  28299  cvmlift2lem10  28425  climuzcnv  28540  fundmpss  28801  preddowncl  28881  soseq  28939  sltres  29029  segconeq  29265  ifscgr  29299  endofsegid  29340  colinbtwnle  29373  onsuct0  29511  trer  29739  ivthALT  29758  fnessref  29793  fnemeet2  29816  fnejoin2  29818  isbnd2  29910  bfplem2  29950  ghomco  29976  cnf1dd  30121  contrd  30128  mpt2bi123f  30203  mptbi12f  30207  jca2  30217  jca2r  30218  prter2  30254  lcmdvdsb  30845  pm11.71  30909  bnj600  33074  bj-finsumval0  33753  bj-bary1  33771  lshpset2N  33934  cvrnbtwn2  34090  cvrnbtwn3  34091  cvrnbtwn4  34094  cvlcvr1  34154  hlrelat2  34217  cvrat4  34257  islpln2a  34362  linepsubN  34566  elpaddn0  34614  paddssw2  34658  pmapjoin  34666  ispsubcl2N  34761  dochkrshp  36201  dochsatshp  36266  mapdh9a  36605  hdmap11lem2  36660