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  3042  disjxiun  4173  oneqmini  4596  oneqmin  4748  iss  5152  funssres  5456  ssimaex  5751  elpreima  5813  isomin  6020  frxp  6419  tposfo2  6465  onfununi  6566  oaordex  6764  oa00  6765  odi  6785  oneo  6787  oeordsuc  6800  oelim2  6801  nnarcl  6822  nnmord  6838  nnneo  6857  map0g  7016  mapsn  7018  domtriord  7216  onomeneq  7259  pssnn  7290  findcard3  7313  unfilem1  7334  fodomfib  7349  inf0  7536  inf3lem3  7545  inf3lem4  7546  tcel  7644  cplem1  7773  karden  7779  fidomtri2  7841  alephordi  7915  cardinfima  7938  alephval3  7951  dfac5lem5  7968  isf34lem4  8217  axcc4  8279  axdc3lem2  8291  zorn2lem4  8339  zorn2lem6  8341  zorn2lem7  8342  fodomb  8364  indpi  8744  genpcl  8845  addclprlem2  8854  ltaddpr  8871  ltexprlem5  8877  suplem1pr  8889  ltlen  9135  mulgt1  9829  sup2  9924  infmrcl  9947  nominpos  10164  uzind  10321  eqreznegel  10521  xrmaxlt  10729  xrltmin  10730  xrmaxle  10731  xrlemin  10732  xmullem2  10804  ccatopth  11735  shftuz  11843  sqreulem  12122  limsupbnd2  12236  mulcn2  12348  sadcaddlem  12928  dvdsgcdb  13003  algcvgblem  13027  rpexp  13079  iserodd  13168  infpnlem1  13237  divsfval  13731  iscatd  13857  posasymb  14368  plttr  14386  joinle  14409  meetle  14416  latnlej  14456  latnlej2  14459  lsmlub  15256  imasrng  15684  unitmulclb  15729  lbspss  16113  lspsneu  16154  lspprat  16184  assapropd  16345  isclo2  17111  cncls2  17295  cncls  17296  cnntr  17297  cnrest2  17308  cmpsub  17421  cmpcld  17423  kgenss  17532  ptpjpre1  17560  txcn  17615  txlm  17637  qtoptop2  17688  cmphaushmeo  17789  fbun  17829  isfild  17847  ssfg  17861  fbasrn  17873  fgtr  17879  ufinffr  17918  rnelfm  17942  fmfnfmlem4  17946  fclsnei  18008  ghmcnp  18101  metrest  18511  icoopnst  18921  iocopnst  18922  dgreq0  20140  plyexmo  20187  cxpeq0  20526  mumullem2  20920  chpchtsum  20960  bposlem7  21031  lgsqr  21087  ubthlem1  22329  axhcompl-zf  22458  ococss  22752  nmopun  23474  elpjrn  23650  stm1addi  23705  stm1add3i  23707  mdsl1i  23781  chrelat2i  23825  atexch  23841  atcvat4i  23857  mdsymlem3  23865  bian1d  23907  eldmgm  24763  subfacval2  24830  cvmlift2lem10  24956  climuzcnv  25065  dedekind  25144  fundmpss  25340  preddowncl  25414  soseq  25472  sltres  25536  segconeq  25852  ifscgr  25886  endofsegid  25927  colinbtwnle  25960  onsuct0  26099  trer  26213  ivthALT  26232  fnessref  26267  fnemeet2  26290  fnejoin2  26292  isbnd2  26386  bfplem2  26426  ghomco  26452  jca2  26585  jca2r  26586  prter2  26624  pm11.71  27468  usg2spthonot0  28090  bnj600  29000  lshpset2N  29606  cvrnbtwn2  29762  cvrnbtwn3  29763  cvrnbtwn4  29766  cvlcvr1  29826  hlrelat2  29889  cvrat4  29929  islpln2a  30034  linepsubN  30238  elpaddn0  30286  paddssw2  30330  pmapjoin  30338  ispsubcl2N  30433  dochkrshp  31873  dochsatshp  31938  mapdh9a  32277  hdmap11lem2  32332
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