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  2995  disjxiun  4122  oneqmini  4546  oneqmin  4699  iss  5101  funssres  5397  ssimaex  5691  elpreima  5752  isomin  5957  frxp  6353  tposfo2  6399  onfununi  6500  oaordex  6698  oa00  6699  odi  6719  oneo  6721  oeordsuc  6734  oelim2  6735  nnarcl  6756  nnmord  6772  nnneo  6791  map0g  6950  mapsn  6952  domtriord  7150  onomeneq  7193  pssnn  7224  findcard3  7247  unfilem1  7268  fodomfib  7283  inf0  7469  inf3lem3  7478  inf3lem4  7479  tcel  7577  cplem1  7706  karden  7712  fidomtri2  7774  alephordi  7848  cardinfima  7871  alephval3  7884  dfac5lem5  7901  isf34lem4  8150  axcc4  8212  axdc3lem2  8224  zorn2lem4  8273  zorn2lem6  8275  zorn2lem7  8276  fodomb  8298  indpi  8678  genpcl  8779  addclprlem2  8788  ltaddpr  8805  ltexprlem5  8811  suplem1pr  8823  ltlen  9069  mulgt1  9762  sup2  9857  infmrcl  9880  nominpos  10097  uzind  10254  eqreznegel  10454  xrmaxlt  10662  xrltmin  10663  xrmaxle  10664  xrlemin  10665  xmullem2  10737  ccatopth  11663  shftuz  11771  sqreulem  12050  limsupbnd2  12164  mulcn2  12276  sadcaddlem  12856  dvdsgcdb  12931  algcvgblem  12955  rpexp  13007  iserodd  13096  infpnlem1  13165  divsfval  13659  iscatd  13785  posasymb  14296  plttr  14314  joinle  14337  meetle  14344  latnlej  14384  latnlej2  14387  lsmlub  15184  imasrng  15612  unitmulclb  15657  lbspss  16045  lspsneu  16086  lspprat  16116  assapropd  16277  isclo2  17042  cncls2  17219  cncls  17220  cnntr  17221  cnrest2  17231  cmpsub  17344  cmpcld  17346  kgenss  17455  ptpjpre1  17483  txcn  17537  txlm  17559  qtoptop2  17607  cmphaushmeo  17708  fbun  17748  isfild  17766  ssfg  17780  fbasrn  17792  fgtr  17798  ufinffr  17837  rnelfm  17861  fmfnfmlem4  17865  fclsnei  17927  ghmcnp  18010  metrest  18283  icoopnst  18652  iocopnst  18653  dgreq0  19861  plyexmo  19908  cxpeq0  20247  mumullem2  20641  chpchtsum  20681  bposlem7  20752  lgsqr  20808  ex-natded5.3-2  21106  ubthlem1  21762  axhcompl-zf  21891  ococss  22185  nmopun  22907  elpjrn  23083  stm1addi  23138  stm1add3i  23140  mdsl1i  23214  chrelat2i  23258  atexch  23274  atcvat4i  23290  mdsymlem3  23298  bian1d  23342  eldmgm  24254  subfacval2  24321  cvmlift2lem10  24446  climuzcnv  24591  dedekind  24671  fundmpss  24863  preddowncl  24937  soseq  24995  sltres  25059  segconeq  25375  ifscgr  25409  endofsegid  25450  colinbtwnle  25483  onsuct0  25622  trer  25734  ivthALT  25765  fnessref  25800  fnemeet2  25823  fnejoin2  25825  isbnd2  26013  bfplem2  26053  ghomco  26079  jca2  26214  jca2r  26215  prter2  26255  pm11.71  27102  bnj600  28715  lshpset2N  29380  cvrnbtwn2  29536  cvrnbtwn3  29537  cvrnbtwn4  29540  cvlcvr1  29600  hlrelat2  29663  cvrat4  29703  islpln2a  29808  linepsubN  30012  elpaddn0  30060  paddssw2  30104  pmapjoin  30112  ispsubcl2N  30207  dochkrshp  31647  dochsatshp  31712  mapdh9a  32051  hdmap11lem2  32106
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