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

Theorem jcad 530
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 445 . 2  |-  ( ch 
->  ( th  ->  ( ch  /\  th ) ) )
41, 2, 3syl6c 64 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
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  540  jctird  541  ancld  550  ancrd  551  anim12ii  567  oplem1  950  rr19.28v  3095  disjxiun  4281  oneqmini  4761  iss  5146  funssres  5450  ssimaex  5748  elpreima  5815  isomin  6019  oneqmin  6409  frxp  6675  tposfo2  6761  onfununi  6792  oaordex  6989  oa00  6990  odi  7010  oneo  7012  oeordsuc  7025  oelim2  7026  nnarcl  7047  nnmord  7063  nnneo  7082  map0g  7244  mapsn  7246  domtriord  7449  onomeneq  7492  pssnn  7523  findcard3  7547  unfilem1  7568  fodomfib  7583  inf0  7819  inf3lem3  7828  inf3lem4  7829  tcel  7957  cplem1  8088  karden  8094  fidomtri2  8156  alephordi  8236  cardinfima  8259  alephval3  8272  dfac5lem5  8289  isf34lem4  8538  axcc4  8600  axdc3lem2  8612  zorn2lem4  8660  zorn2lem6  8662  zorn2lem7  8663  fodomb  8685  indpi  9068  genpcl  9169  addclprlem2  9178  ltaddpr  9195  ltexprlem5  9201  suplem1pr  9213  ltlen  9468  dedekind  9525  mulgt1  10180  sup2  10278  infmrcl  10301  nominpos  10553  uzind  10725  eqreznegel  10932  xrmaxlt  11145  xrltmin  11146  xrmaxle  11147  xrlemin  11148  xmullem2  11220  ccatopth  12352  shftuz  12546  sqreulem  12835  limsupbnd2  12949  mulcn2  13061  sadcaddlem  13640  dvdsgcdb  13715  algcvgblem  13739  rpexp  13793  iserodd  13889  infpnlem1  13958  divsfval  14472  iscatd  14598  posasymb  15109  plttr  15127  joinle  15171  meetle  15185  latnlej  15225  latnlej2  15228  lsmlub  16146  imasrng  16650  unitmulclb  16695  lbspss  17089  lspsneu  17130  lspprat  17160  assapropd  17324  isclo2  18538  cncls2  18723  cncls  18724  cnntr  18725  cnrest2  18736  cmpsub  18849  cmpcld  18851  kgenss  18962  ptpjpre1  18990  txcn  19045  txlm  19067  qtoptop2  19118  cmphaushmeo  19219  fbun  19259  isfild  19277  ssfg  19291  fbasrn  19303  fgtr  19309  ufinffr  19348  rnelfm  19372  fmfnfmlem4  19376  fclsnei  19438  ghmcnp  19531  metrest  19945  icoopnst  20357  iocopnst  20358  dgreq0  21621  plyexmo  21668  cxpeq0  22012  mumullem2  22407  chpchtsum  22447  bposlem7  22518  lgsqr  22574  ex-natded5.3-2  23442  ubthlem1  24098  axhcompl-zf  24227  ococss  24523  nmopun  25245  elpjrn  25421  stm1addi  25476  stm1add3i  25478  mdsl1i  25552  chrelat2i  25596  atexch  25612  atcvat4i  25628  mdsymlem3  25636  bian1d  25678  eldmgm  26860  subfacval2  26927  cvmlift2lem10  27053  climuzcnv  27167  fundmpss  27428  preddowncl  27508  soseq  27566  sltres  27656  segconeq  27892  ifscgr  27926  endofsegid  27967  colinbtwnle  28000  onsuct0  28139  trer  28359  ivthALT  28378  fnessref  28413  fnemeet2  28436  fnejoin2  28438  isbnd2  28530  bfplem2  28570  ghomco  28596  cnf1dd  28741  contrd  28748  jca2  28838  jca2r  28839  prter2  28875  pm11.71  29499  usg2wlkeq  30139  usg2spthonot0  30258  bnj600  31677  bj-finsumval0  32222  bj-bary1  32239  lshpset2N  32400  cvrnbtwn2  32556  cvrnbtwn3  32557  cvrnbtwn4  32560  cvlcvr1  32620  hlrelat2  32683  cvrat4  32723  islpln2a  32828  linepsubN  33032  elpaddn0  33080  paddssw2  33124  pmapjoin  33132  ispsubcl2N  33227  dochkrshp  34667  dochsatshp  34732  mapdh9a  35071  hdmap11lem2  35126
  Copyright terms: Public domain W3C validator