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

Theorem jcad 554
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 462 . 2 (𝜒 → (𝜃 → (𝜒𝜃)))
41, 2, 3syl6c 70 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  jca2  555  jctild  565  jctird  566  ancld  575  ancrd  576  anim12ii  593  oplem1  1027  2eu1  2582  rr19.28v  3378  disjxiun  4681  disjxiunOLD  4682  iss  5482  preddowncl  5745  oneqmini  5814  funssres  5968  ssimaex  6302  elpreima  6377  isomin  6627  oneqmin  7047  frxp  7332  tposfo2  7420  onfununi  7483  oaordex  7683  oa00  7684  odi  7704  oneo  7706  oeordsuc  7719  oelim2  7720  nnarcl  7741  nnmord  7757  nnneo  7776  map0g  7939  mapsn  7941  domtriord  8147  onomeneq  8191  pssnn  8219  findcard3  8244  unfilem1  8265  fodomfib  8281  inf0  8556  inf3lem3  8565  inf3lem4  8566  tcel  8659  cplem1  8790  karden  8796  fidomtri2  8858  alephordi  8935  cardinfima  8958  alephval3  8971  dfac5lem5  8988  isf34lem4  9237  axcc4  9299  axdc3lem2  9311  zorn2lem4  9359  zorn2lem6  9361  zorn2lem7  9362  fodomb  9386  indpi  9767  genpcl  9868  addclprlem2  9877  ltaddpr  9894  ltexprlem5  9900  suplem1pr  9912  ltlen  10176  dedekind  10238  mulgt1  10920  sup2  11017  nominpos  11307  uzind  11507  eqreznegel  11812  xrmaxlt  12050  xrltmin  12051  xrmaxle  12052  xrlemin  12053  xmullem2  12133  ccatopth  13516  shftuz  13853  sqreulem  14143  limsupbnd2  14258  mulcn2  14370  sadcaddlem  15226  dvdsgcdb  15309  algcvgblem  15337  lcmdvdsb  15373  rpexp  15479  iserodd  15587  infpnlem1  15661  divsfval  16254  iscatd  16381  posasymb  16999  plttr  17017  joinle  17061  meetle  17075  latnlej  17115  latnlej2  17118  lsmlub  18124  imasring  18665  unitmulclb  18711  lbspss  19130  lspsneu  19171  lspprat  19201  assapropd  19375  isclo2  20940  cncls2  21125  cncls  21126  cnntr  21127  cnrest2  21138  cmpsub  21251  cmpcld  21253  kgenss  21394  ptpjpre1  21422  txcn  21477  txlm  21499  qtoptop2  21550  cmphaushmeo  21651  fbun  21691  isfild  21709  ssfg  21723  fbasrn  21735  fgtr  21741  ufinffr  21780  rnelfm  21804  fmfnfmlem4  21808  fclsnei  21870  ghmcnp  21965  metrest  22376  icoopnst  22785  iocopnst  22786  dgreq0  24066  plyexmo  24113  cxpeq0  24469  eldmgm  24793  mumullem2  24951  chpchtsum  24989  bposlem7  25060  lgsqr  25121  uspgr2wlkeq  26598  wwlknllvtx  26795  ex-natded5.3-2  27395  ubthlem1  27854  axhcompl-zf  27983  ococss  28280  nmopun  29001  elpjrn  29177  stm1addi  29232  stm1add3i  29234  mdsl1i  29308  chrelat2i  29352  atexch  29368  atcvat4i  29384  mdsymlem3  29392  bian1d  29434  bnj600  31115  subfacval2  31295  climuzcnv  31691  fundmpss  31790  soseq  31879  sltres  31940  nosupno  31974  segconeq  32242  ifscgr  32276  endofsegid  32317  colinbtwnle  32350  trer  32435  ivthALT  32455  fnessref  32477  fnemeet2  32487  fnejoin2  32489  onsuct0  32565  bj-finsumval0  33277  bj-bary1  33292  icorempt2  33329  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlpssretop  33342  finxpsuclem  33364  poimirlem31  33570  isbnd2  33712  bfplem2  33752  ghomco  33820  cnf1dd  34022  contrd  34029  mpt2bi123f  34101  mptbi12f  34105  iss2  34252  jca2r  34458  prter2  34485  lshpset2N  34724  cvrnbtwn2  34880  cvrnbtwn3  34881  cvrnbtwn4  34884  cvlcvr1  34944  hlrelat2  35007  cvrat4  35047  islpln2a  35152  linepsubN  35356  elpaddn0  35404  paddssw2  35448  pmapjoin  35456  ispsubcl2N  35551  dochkrshp  36992  dochsatshp  37057  mapdh9a  37396  hdmap11lem2  37451  pwinfi3  38185  rfovcnvf1od  38615  clsk1independent  38661  gneispace  38749  pm11.71  38914  sbgoldbaltlem2  41993  setrec1lem4  42762
  Copyright terms: Public domain W3C validator