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

Theorem jcad 533
Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
jcad.1
jcad.2
Assertion
Ref Expression
jcad

Proof of Theorem jcad
StepHypRef Expression
1 jcad.1 . 2
2 jcad.2 . 2
3 pm3.2 447 . 2
41, 2, 3syl6c 64 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  jctild  543  jctird  544  ancld  553  ancrd  554  anim12ii  570  oplem1  964  2eu1  2376  rr19.28v  3242  disjxiun  4449  oneqmini  4934  iss  5326  funssres  5633  ssimaex  5938  elpreima  6007  isomin  6233  oneqmin  6640  frxp  6910  tposfo2  6997  onfununi  7031  oaordex  7226  oa00  7227  odi  7247  oneo  7249  oeordsuc  7262  oelim2  7263  nnarcl  7284  nnmord  7300  nnneo  7319  map0g  7478  mapsn  7480  domtriord  7683  onomeneq  7727  pssnn  7758  findcard3  7783  unfilem1  7804  fodomfib  7820  inf0  8059  inf3lem3  8068  inf3lem4  8069  tcel  8197  cplem1  8328  karden  8334  fidomtri2  8396  alephordi  8476  cardinfima  8499  alephval3  8512  dfac5lem5  8529  isf34lem4  8778  axcc4  8840  axdc3lem2  8852  zorn2lem4  8900  zorn2lem6  8902  zorn2lem7  8903  fodomb  8925  indpi  9306  genpcl  9407  addclprlem2  9416  ltaddpr  9433  ltexprlem5  9439  suplem1pr  9451  ltlen  9707  dedekind  9765  mulgt1  10426  sup2  10524  infmrcl  10547  nominpos  10800  uzind  10979  eqreznegel  11196  xrmaxlt  11411  xrltmin  11412  xrmaxle  11413  xrlemin  11414  xmullem2  11486  ccatopth  12695  shftuz  12902  sqreulem  13192  limsupbnd2  13306  mulcn2  13418  sadcaddlem  14107  dvdsgcdb  14182  algcvgblem  14206  rpexp  14261  iserodd  14359  infpnlem1  14428  divsfval  14944  iscatd  15070  posasymb  15582  plttr  15600  joinle  15644  meetle  15658  latnlej  15698  latnlej2  15701  lsmlub  16683  imasring  17268  unitmulclb  17314  lbspss  17728  lspsneu  17769  lspprat  17799  assapropd  17976  isclo2  19589  cncls2  19774  cncls  19775  cnntr  19776  cnrest2  19787  cmpsub  19900  cmpcld  19902  kgenss  20044  ptpjpre1  20072  txcn  20127  txlm  20149  qtoptop2  20200  cmphaushmeo  20301  fbun  20341  isfild  20359  ssfg  20373  fbasrn  20385  fgtr  20391  ufinffr  20430  rnelfm  20454  fmfnfmlem4  20458  fclsnei  20520  ghmcnp  20613  metrest  21027  icoopnst  21439  iocopnst  21440  dgreq0  22662  plyexmo  22709  cxpeq0  23059  mumullem2  23454  chpchtsum  23494  bposlem7  23565  lgsqr  23621  usg2wlkeq  24708  usg2spthonot0  24889  ex-natded5.3-2  25129  ubthlem1  25786  axhcompl-zf  25915  ococss  26211  nmopun  26933  elpjrn  27109  stm1addi  27164  stm1add3i  27166  mdsl1i  27240  chrelat2i  27284  atexch  27300  atcvat4i  27316  mdsymlem3  27324  bian1d  27366  eldmgm  28564  subfacval2  28631  cvmlift2lem10  28757  climuzcnv  29037  fundmpss  29196  preddowncl  29276  soseq  29334  sltres  29424  segconeq  29660  ifscgr  29694  endofsegid  29735  colinbtwnle  29768  onsuct0  29906  trer  30134  ivthALT  30153  fnessref  30175  fnemeet2  30185  fnejoin2  30187  isbnd2  30279  bfplem2  30319  ghomco  30345  cnf1dd  30490  contrd  30497  mpt2bi123f  30571  mptbi12f  30575  jca2  30585  jca2r  30586  prter2  30622  lcmdvdsb  31217  pm11.71  31303  bnj600  33977  bj-finsumval0  34663  bj-bary1  34681  lshpset2N  34844  cvrnbtwn2  35000  cvrnbtwn3  35001  cvrnbtwn4  35004  cvlcvr1  35064  hlrelat2  35127  cvrat4  35167  islpln2a  35272  linepsubN  35476  elpaddn0  35524  paddssw2  35568  pmapjoin  35576  ispsubcl2N  35671  dochkrshp  37113  dochsatshp  37178  mapdh9a  37517  hdmap11lem2  37572  pwinfi3  37748
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
  Copyright terms: Public domain W3C validator