MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jcad Unicode version

Theorem jcad 519
Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-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
StepHypRef Expression
1 jcad.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 jcad.2 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 pm3.2 434 . 2  |-  ( ch 
->  ( th  ->  ( ch  /\  th ) ) )
41, 2, 3syl6c 60 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  jctild  527  jctird  528  ancld  536  ancrd  537  anim12ii  553  oplem1  930  rr19.28v  2910  disjxiun  4020  oneqmini  4443  oneqmin  4596  iss  4998  funssres  5294  ssimaex  5584  elpreima  5645  isomin  5834  frxp  6225  tposfo2  6257  onfununi  6358  oaordex  6556  oa00  6557  odi  6577  oneo  6579  oeordsuc  6592  oelim2  6593  nnarcl  6614  nnmord  6630  nnneo  6649  map0g  6807  mapsn  6809  domtriord  7007  onomeneq  7050  pssnn  7081  findcard3  7100  unfilem1  7121  fodomfib  7136  inf0  7322  inf3lem3  7331  inf3lem4  7332  tcel  7430  cplem1  7559  karden  7565  fidomtri2  7627  alephordi  7701  cardinfima  7724  alephval3  7737  dfac5lem5  7754  isf34lem4  8003  axcc4  8065  axdc3lem2  8077  zorn2lem4  8126  zorn2lem6  8128  zorn2lem7  8129  fodomb  8151  indpi  8531  genpcl  8632  addclprlem2  8641  ltaddpr  8658  ltexprlem5  8664  suplem1pr  8676  ltlen  8922  mulgt1  9615  sup2  9710  infmrcl  9733  nominpos  9948  uzind  10103  eqreznegel  10303  xrmaxlt  10510  xrltmin  10511  xrmaxle  10512  xrlemin  10513  xmullem2  10585  ccatopth  11462  shftuz  11564  sqreulem  11843  limsupbnd2  11957  mulcn2  12069  sadcaddlem  12648  dvdsgcdb  12723  algcvgblem  12747  rpexp  12799  iserodd  12888  infpnlem1  12957  divsfval  13449  iscatd  13575  posasymb  14086  plttr  14104  joinle  14127  meetle  14134  latnlej  14174  latnlej2  14177  lsmlub  14974  imasrng  15402  unitmulclb  15447  lbspss  15835  lspsneu  15876  lspprat  15906  assapropd  16067  isclo2  16825  cncls2  17002  cncls  17003  cnntr  17004  cnrest2  17014  cmpsub  17127  cmpcld  17129  kgenss  17238  ptpjpre1  17266  txcn  17320  txlm  17342  qtoptop2  17390  cmphaushmeo  17491  fbun  17535  isfild  17553  ssfg  17567  fbasrn  17579  fgtr  17585  ufinffr  17624  rnelfm  17648  fmfnfmlem4  17652  fclsnei  17714  ghmcnp  17797  metrest  18070  icoopnst  18437  iocopnst  18438  dgreq0  19646  plyexmo  19693  cxpeq0  20025  mumullem2  20418  chpchtsum  20458  bposlem7  20529  lgsqr  20585  ex-natded5.3-2  20795  ubthlem1  21449  axhcompl-zf  21578  ococss  21872  nmopun  22594  elpjrn  22770  stm1addi  22825  stm1add3i  22827  mdsl1i  22901  chrelat2i  22945  atexch  22961  atcvat4i  22977  mdsymlem3  22985  bian1d  23122  eldmgm  23694  subfacval2  23718  cvmlift2lem10  23843  climuzcnv  24004  dedekind  24082  fundmpss  24122  preddowncl  24196  soseq  24254  sltres  24318  segconeq  24633  ifscgr  24667  endofsegid  24708  colinbtwnle  24741  onsuct0  24880  issubrv  25672  mrdmcd  25794  cmphmia  25798  cmphmib  25799  ismonc  25814  isepic  25824  trer  26227  ivthALT  26258  fnessref  26293  fnemeet2  26316  fnejoin2  26318  isbnd2  26507  bfplem2  26547  ghomco  26573  jca2  26708  jca2r  26709  prter2  26749  pm11.71  27596  bnj600  28951  lshpset2N  29309  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrnbtwn4  29469  cvlcvr1  29529  hlrelat2  29592  cvrat4  29632  islpln2a  29737  linepsubN  29941  elpaddn0  29989  paddssw2  30033  pmapjoin  30041  ispsubcl2N  30136  dochkrshp  31576  dochsatshp  31641  mapdh9a  31980  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator