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

Theorem jcad 521
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 436 . 2  |-  ( ch 
->  ( th  ->  ( ch  /\  th ) ) )
41, 2, 3syl6c 63 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  jctild  529  jctird  530  ancld  538  ancrd  539  anim12ii  555  oplem1  932  rr19.28v  3080  disjxiun  4212  oneqmini  4635  oneqmin  4788  iss  5192  funssres  5496  ssimaex  5791  elpreima  5853  isomin  6060  frxp  6459  tposfo2  6505  onfununi  6606  oaordex  6804  oa00  6805  odi  6825  oneo  6827  oeordsuc  6840  oelim2  6841  nnarcl  6862  nnmord  6878  nnneo  6897  map0g  7056  mapsn  7058  domtriord  7256  onomeneq  7299  pssnn  7330  findcard3  7353  unfilem1  7374  fodomfib  7389  inf0  7579  inf3lem3  7588  inf3lem4  7589  tcel  7687  cplem1  7818  karden  7824  fidomtri2  7886  alephordi  7960  cardinfima  7983  alephval3  7996  dfac5lem5  8013  isf34lem4  8262  axcc4  8324  axdc3lem2  8336  zorn2lem4  8384  zorn2lem6  8386  zorn2lem7  8387  fodomb  8409  indpi  8789  genpcl  8890  addclprlem2  8899  ltaddpr  8916  ltexprlem5  8922  suplem1pr  8934  ltlen  9180  mulgt1  9874  sup2  9969  infmrcl  9992  nominpos  10209  uzind  10366  eqreznegel  10566  xrmaxlt  10774  xrltmin  10775  xrmaxle  10776  xrlemin  10777  xmullem2  10849  ccatopth  11781  shftuz  11889  sqreulem  12168  limsupbnd2  12282  mulcn2  12394  sadcaddlem  12974  dvdsgcdb  13049  algcvgblem  13073  rpexp  13125  iserodd  13214  infpnlem1  13283  divsfval  13777  iscatd  13903  posasymb  14414  plttr  14432  joinle  14455  meetle  14462  latnlej  14502  latnlej2  14505  lsmlub  15302  imasrng  15730  unitmulclb  15775  lbspss  16159  lspsneu  16200  lspprat  16230  assapropd  16391  isclo2  17157  cncls2  17342  cncls  17343  cnntr  17344  cnrest2  17355  cmpsub  17468  cmpcld  17470  kgenss  17580  ptpjpre1  17608  txcn  17663  txlm  17685  qtoptop2  17736  cmphaushmeo  17837  fbun  17877  isfild  17895  ssfg  17909  fbasrn  17921  fgtr  17927  ufinffr  17966  rnelfm  17990  fmfnfmlem4  17994  fclsnei  18056  ghmcnp  18149  metrest  18559  icoopnst  18969  iocopnst  18970  dgreq0  20188  plyexmo  20235  cxpeq0  20574  mumullem2  20968  chpchtsum  21008  bposlem7  21079  lgsqr  21135  ubthlem1  22377  axhcompl-zf  22506  ococss  22800  nmopun  23522  elpjrn  23698  stm1addi  23753  stm1add3i  23755  mdsl1i  23829  chrelat2i  23873  atexch  23889  atcvat4i  23905  mdsymlem3  23913  bian1d  23955  eldmgm  24811  subfacval2  24878  cvmlift2lem10  25004  climuzcnv  25113  dedekind  25192  fundmpss  25395  preddowncl  25476  soseq  25534  sltres  25624  segconeq  25949  ifscgr  25983  endofsegid  26024  colinbtwnle  26057  onsuct0  26196  trer  26333  ivthALT  26352  fnessref  26387  fnemeet2  26410  fnejoin2  26412  isbnd2  26506  bfplem2  26546  ghomco  26572  jca2  26705  jca2r  26706  prter2  26744  pm11.71  27587  usg2wlkeq  28342  usg2spthonot0  28421  bnj600  29364  lshpset2N  29991  cvrnbtwn2  30147  cvrnbtwn3  30148  cvrnbtwn4  30151  cvlcvr1  30211  hlrelat2  30274  cvrat4  30314  islpln2a  30419  linepsubN  30623  elpaddn0  30671  paddssw2  30715  pmapjoin  30723  ispsubcl2N  30818  dochkrshp  32258  dochsatshp  32323  mapdh9a  32662  hdmap11lem2  32717
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 179  df-an 362
  Copyright terms: Public domain W3C validator