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

Theorem jcad 520
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 435 . 2  |-  ( ch 
->  ( th  ->  ( ch  /\  th ) ) )
41, 2, 3syl6c 62 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  jctild  528  jctird  529  ancld  537  ancrd  538  anim12ii  554  oplem1  931  rr19.28v  3038  disjxiun  4169  oneqmini  4592  oneqmin  4744  iss  5148  funssres  5452  ssimaex  5747  elpreima  5809  isomin  6016  frxp  6415  tposfo2  6461  onfununi  6562  oaordex  6760  oa00  6761  odi  6781  oneo  6783  oeordsuc  6796  oelim2  6797  nnarcl  6818  nnmord  6834  nnneo  6853  map0g  7012  mapsn  7014  domtriord  7212  onomeneq  7255  pssnn  7286  findcard3  7309  unfilem1  7330  fodomfib  7345  inf0  7532  inf3lem3  7541  inf3lem4  7542  tcel  7640  cplem1  7769  karden  7775  fidomtri2  7837  alephordi  7911  cardinfima  7934  alephval3  7947  dfac5lem5  7964  isf34lem4  8213  axcc4  8275  axdc3lem2  8287  zorn2lem4  8335  zorn2lem6  8337  zorn2lem7  8338  fodomb  8360  indpi  8740  genpcl  8841  addclprlem2  8850  ltaddpr  8867  ltexprlem5  8873  suplem1pr  8885  ltlen  9131  mulgt1  9825  sup2  9920  infmrcl  9943  nominpos  10160  uzind  10317  eqreznegel  10517  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  xmullem2  10800  ccatopth  11731  shftuz  11839  sqreulem  12118  limsupbnd2  12232  mulcn2  12344  sadcaddlem  12924  dvdsgcdb  12999  algcvgblem  13023  rpexp  13075  iserodd  13164  infpnlem1  13233  divsfval  13727  iscatd  13853  posasymb  14364  plttr  14382  joinle  14405  meetle  14412  latnlej  14452  latnlej2  14455  lsmlub  15252  imasrng  15680  unitmulclb  15725  lbspss  16109  lspsneu  16150  lspprat  16180  assapropd  16341  isclo2  17107  cncls2  17291  cncls  17292  cnntr  17293  cnrest2  17304  cmpsub  17417  cmpcld  17419  kgenss  17528  ptpjpre1  17556  txcn  17611  txlm  17633  qtoptop2  17684  cmphaushmeo  17785  fbun  17825  isfild  17843  ssfg  17857  fbasrn  17869  fgtr  17875  ufinffr  17914  rnelfm  17938  fmfnfmlem4  17942  fclsnei  18004  ghmcnp  18097  metrest  18507  icoopnst  18917  iocopnst  18918  dgreq0  20136  plyexmo  20183  cxpeq0  20522  mumullem2  20916  chpchtsum  20956  bposlem7  21027  lgsqr  21083  ubthlem1  22325  axhcompl-zf  22454  ococss  22748  nmopun  23470  elpjrn  23646  stm1addi  23701  stm1add3i  23703  mdsl1i  23777  chrelat2i  23821  atexch  23837  atcvat4i  23853  mdsymlem3  23861  bian1d  23903  eldmgm  24759  subfacval2  24826  cvmlift2lem10  24952  climuzcnv  25061  dedekind  25140  fundmpss  25336  preddowncl  25410  soseq  25468  sltres  25532  segconeq  25848  ifscgr  25882  endofsegid  25923  colinbtwnle  25956  onsuct0  26095  trer  26209  ivthALT  26228  fnessref  26263  fnemeet2  26286  fnejoin2  26288  isbnd2  26382  bfplem2  26422  ghomco  26448  jca2  26581  jca2r  26582  prter2  26620  pm11.71  27464  usg2spthonot0  28086  bnj600  28996  lshpset2N  29602  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrnbtwn4  29762  cvlcvr1  29822  hlrelat2  29885  cvrat4  29925  islpln2a  30030  linepsubN  30234  elpaddn0  30282  paddssw2  30326  pmapjoin  30334  ispsubcl2N  30429  dochkrshp  31869  dochsatshp  31934  mapdh9a  32273  hdmap11lem2  32328
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 178  df-an 361
  Copyright terms: Public domain W3C validator