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  964  2eu1  2362  rr19.28v  3228  disjxiun  4434  oneqmini  4919  iss  5311  funssres  5618  ssimaex  5923  elpreima  5992  isomin  6218  oneqmin  6625  frxp  6895  tposfo2  6980  onfununi  7014  oaordex  7209  oa00  7210  odi  7230  oneo  7232  oeordsuc  7245  oelim2  7246  nnarcl  7267  nnmord  7283  nnneo  7302  map0g  7460  mapsn  7462  domtriord  7665  onomeneq  7709  pssnn  7740  findcard3  7765  unfilem1  7786  fodomfib  7802  inf0  8041  inf3lem3  8050  inf3lem4  8051  tcel  8179  cplem1  8310  karden  8316  fidomtri2  8378  alephordi  8458  cardinfima  8481  alephval3  8494  dfac5lem5  8511  isf34lem4  8760  axcc4  8822  axdc3lem2  8834  zorn2lem4  8882  zorn2lem6  8884  zorn2lem7  8885  fodomb  8907  indpi  9288  genpcl  9389  addclprlem2  9398  ltaddpr  9415  ltexprlem5  9421  suplem1pr  9433  ltlen  9689  dedekind  9747  mulgt1  10407  sup2  10505  infmrcl  10528  nominpos  10781  uzind  10960  eqreznegel  11176  xrmaxlt  11391  xrltmin  11392  xrmaxle  11393  xrlemin  11394  xmullem2  11466  ccatopth  12674  shftuz  12881  sqreulem  13171  limsupbnd2  13285  mulcn2  13397  sadcaddlem  13984  dvdsgcdb  14059  algcvgblem  14083  rpexp  14138  iserodd  14236  infpnlem1  14305  divsfval  14821  iscatd  14947  posasymb  15456  plttr  15474  joinle  15518  meetle  15532  latnlej  15572  latnlej2  15575  lsmlub  16557  imasring  17142  unitmulclb  17188  lbspss  17602  lspsneu  17643  lspprat  17673  assapropd  17850  isclo2  19462  cncls2  19647  cncls  19648  cnntr  19649  cnrest2  19660  cmpsub  19773  cmpcld  19775  kgenss  19917  ptpjpre1  19945  txcn  20000  txlm  20022  qtoptop2  20073  cmphaushmeo  20174  fbun  20214  isfild  20232  ssfg  20246  fbasrn  20258  fgtr  20264  ufinffr  20303  rnelfm  20327  fmfnfmlem4  20331  fclsnei  20393  ghmcnp  20486  metrest  20900  icoopnst  21312  iocopnst  21313  dgreq0  22534  plyexmo  22581  cxpeq0  22931  mumullem2  23326  chpchtsum  23366  bposlem7  23437  lgsqr  23493  usg2wlkeq  24580  usg2spthonot0  24761  ex-natded5.3-2  25001  ubthlem1  25658  axhcompl-zf  25787  ococss  26083  nmopun  26805  elpjrn  26981  stm1addi  27036  stm1add3i  27038  mdsl1i  27112  chrelat2i  27156  atexch  27172  atcvat4i  27188  mdsymlem3  27196  bian1d  27238  eldmgm  28437  subfacval2  28504  cvmlift2lem10  28630  climuzcnv  28910  fundmpss  29171  preddowncl  29251  soseq  29309  sltres  29399  segconeq  29635  ifscgr  29669  endofsegid  29710  colinbtwnle  29743  onsuct0  29881  trer  30109  ivthALT  30128  fnessref  30150  fnemeet2  30160  fnejoin2  30162  isbnd2  30254  bfplem2  30294  ghomco  30320  cnf1dd  30465  contrd  30472  mpt2bi123f  30546  mptbi12f  30550  jca2  30560  jca2r  30561  prter2  30597  lcmdvdsb  31193  pm11.71  31257  bnj600  33705  bj-finsumval0  34397  bj-bary1  34415  lshpset2N  34578  cvrnbtwn2  34734  cvrnbtwn3  34735  cvrnbtwn4  34738  cvlcvr1  34798  hlrelat2  34861  cvrat4  34901  islpln2a  35006  linepsubN  35210  elpaddn0  35258  paddssw2  35302  pmapjoin  35310  ispsubcl2N  35405  dochkrshp  36847  dochsatshp  36912  mapdh9a  37251  hdmap11lem2  37306  pwinfi3  37445