Theorem jcad 540

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  jctild  550  jctird  551  ancld  560  ancrd  561  anim12ii  578  oplem1  981  2eu1  2392  rr19.28v  3192  disjxiun  4412  iss  5170  preddowncl  5425  oneqmini  5492  funssres  5640  ssimaex  5952  elpreima  6024  isomin  6252  oneqmin  6658  frxp  6932  tposfo2  7021  onfununi  7085  oaordex  7284  oa00  7285  odi  7305  oneo  7307  oeordsuc  7320  oelim2  7321  nnarcl  7342  nnmord  7358  nnneo  7377  map0g  7536  mapsn  7538  domtriord  7743  onomeneq  7787  pssnn  7815  findcard3  7839  unfilem1  7860  fodomfib  7876  inf0  8151  inf3lem3  8160  inf3lem4  8161  tcel  8254  cplem1  8385  karden  8391  fidomtri2  8453  alephordi  8530  cardinfima  8553  alephval3  8566  dfac5lem5  8583  isf34lem4  8832  axcc4  8894  axdc3lem2  8906  zorn2lem4  8954  zorn2lem6  8956  zorn2lem7  8957  fodomb  8979  indpi  9357  genpcl  9458  addclprlem2  9467  ltaddpr  9484  ltexprlem5  9490  suplem1pr  9502  ltlen  9760  dedekind  9822  mulgt1  10491  sup2  10592  infmrclOLD  10620  nominpos  10877  uzind  11055  eqreznegel  11277  xrmaxlt  11504  xrltmin  11505  xrmaxle  11506  xrlemin  11507  xmullem2  11579  ccatopth  12862  shftuz  13180  sqreulem  13470  limsupbnd2  13594  limsupbnd2OLD  13595  mulcn2  13707  sadcaddlem  14479  dvdsgcdb  14560  algcvgblem  14584  lcmdvdsb  14626  rpexp  14720  iserodd  14833  infpnlem1  14902  divsfval  15501  iscatd  15627  posasymb  16246  plttr  16264  joinle  16308  meetle  16322  latnlej  16362  latnlej2  16365  lsmlub  17363  imasring  17895  unitmulclb  17941  lbspss  18353  lspsneu  18394  lspprat  18424  assapropd  18599  isclo2  20152  cncls2  20337  cncls  20338  cnntr  20339  cnrest2  20350  cmpsub  20463  cmpcld  20465  kgenss  20606  ptpjpre1  20634  txcn  20689  txlm  20711  qtoptop2  20762  cmphaushmeo  20863  fbun  20903  isfild  20921  ssfg  20935  fbasrn  20947  fgtr  20953  ufinffr  20992  rnelfm  21016  fmfnfmlem4  21020  fclsnei  21082  ghmcnp  21177  metrest  21587  icoopnst  22015  iocopnst  22016  dgreq0  23267  plyexmo  23314  cxpeq0  23671  eldmgm  23995  mumullem2  24155  chpchtsum  24195  bposlem7  24266  lgsqr  24322  usg2wlkeq  25484  usg2spthonot0  25665  ex-natded5.3-2  25906  ubthlem1  26560  axhcompl-zf  26699  ococss  26994  nmopun  27715  elpjrn  27891  stm1addi  27946  stm1add3i  27948  mdsl1i  28022  chrelat2i  28066  atexch  28082  atcvat4i  28098  mdsymlem3  28106  bian1d  28148  bnj600  29778  subfacval2  29958  cvmlift2lem10  30083  climuzcnv  30363  fundmpss  30455  soseq  30540  sltres  30599  segconeq  30825  ifscgr  30859  endofsegid  30900  colinbtwnle  30933  trer  31020  ivthALT  31039  fnessref  31061  fnemeet2  31071  fnejoin2  31073  onsuct0  31149  bj-finsumval0  31746  bj-bary1  31761  icorempt2  31798  isbasisrelowllem1  31802  isbasisrelowllem2  31803  relowlpssretop  31811  finxpsuclem  31833  poimirlem31  32015  isbnd2  32159  bfplem2  32199  ghomco  32225  cnf1dd  32370  contrd  32377  mpt2bi123f  32450  mptbi12f  32454  jca2  32464  jca2r  32465  prter2  32497  lshpset2N  32729  cvrnbtwn2  32885  cvrnbtwn3  32886  cvrnbtwn4  32889  cvlcvr1  32949  hlrelat2  33012  cvrat4  33052  islpln2a  33157  linepsubN  33361  elpaddn0  33409  paddssw2  33453  pmapjoin  33461  ispsubcl2N  33556  dochkrshp  34998  dochsatshp  35063  mapdh9a  35402  hdmap11lem2  35457  pwinfi3  36211  pm11.71  36790  sgoldbaltlem2  38918