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 68 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 196  df-an 385
This theorem is referenced by:  jctild  564  jctird  565  ancld  574  ancrd  575  anim12ii  592  oplem1  999  2eu1  2541  rr19.28v  3315  disjxiun  4579  disjxiunOLD  4580  iss  5367  preddowncl  5624  oneqmini  5693  funssres  5844  ssimaex  6173  elpreima  6245  isomin  6487  oneqmin  6897  frxp  7174  tposfo2  7262  onfununi  7325  oaordex  7525  oa00  7526  odi  7546  oneo  7548  oeordsuc  7561  oelim2  7562  nnarcl  7583  nnmord  7599  nnneo  7618  map0g  7783  mapsn  7785  domtriord  7991  onomeneq  8035  pssnn  8063  findcard3  8088  unfilem1  8109  fodomfib  8125  inf0  8401  inf3lem3  8410  inf3lem4  8411  tcel  8504  cplem1  8635  karden  8641  fidomtri2  8703  alephordi  8780  cardinfima  8803  alephval3  8816  dfac5lem5  8833  isf34lem4  9082  axcc4  9144  axdc3lem2  9156  zorn2lem4  9204  zorn2lem6  9206  zorn2lem7  9207  fodomb  9229  indpi  9608  genpcl  9709  addclprlem2  9718  ltaddpr  9735  ltexprlem5  9741  suplem1pr  9753  ltlen  10017  dedekind  10079  mulgt1  10761  sup2  10858  nominpos  11146  uzind  11345  eqreznegel  11650  xrmaxlt  11886  xrltmin  11887  xrmaxle  11888  xrlemin  11889  xmullem2  11967  ccatopth  13322  shftuz  13657  sqreulem  13947  limsupbnd2  14062  mulcn2  14174  sadcaddlem  15017  dvdsgcdb  15100  algcvgblem  15128  lcmdvdsb  15164  rpexp  15270  iserodd  15378  infpnlem1  15452  divsfval  16030  iscatd  16157  posasymb  16775  plttr  16793  joinle  16837  meetle  16851  latnlej  16891  latnlej2  16894  lsmlub  17901  imasring  18442  unitmulclb  18488  lbspss  18903  lspsneu  18944  lspprat  18974  assapropd  19148  isclo2  20702  cncls2  20887  cncls  20888  cnntr  20889  cnrest2  20900  cmpsub  21013  cmpcld  21015  kgenss  21156  ptpjpre1  21184  txcn  21239  txlm  21261  qtoptop2  21312  cmphaushmeo  21413  fbun  21454  isfild  21472  ssfg  21486  fbasrn  21498  fgtr  21504  ufinffr  21543  rnelfm  21567  fmfnfmlem4  21571  fclsnei  21633  ghmcnp  21728  metrest  22139  icoopnst  22546  iocopnst  22547  dgreq0  23825  plyexmo  23872  cxpeq0  24224  eldmgm  24548  mumullem2  24706  chpchtsum  24744  bposlem7  24815  lgsqr  24876  usg2wlkeq  26236  usg2spthonot0  26416  ex-natded5.3-2  26657  ubthlem1  27110  axhcompl-zf  27239  ococss  27536  nmopun  28257  elpjrn  28433  stm1addi  28488  stm1add3i  28490  mdsl1i  28564  chrelat2i  28608  atexch  28624  atcvat4i  28640  mdsymlem3  28648  bian1d  28690  bnj600  30243  subfacval2  30423  cvmlift2lem10  30548  climuzcnv  30819  fundmpss  30910  soseq  30995  sltres  31061  segconeq  31287  ifscgr  31321  endofsegid  31362  colinbtwnle  31395  trer  31480  ivthALT  31500  fnessref  31522  fnemeet2  31532  fnejoin2  31534  onsuct0  31610  bj-finsumval0  32324  bj-bary1  32339  icorempt2  32375  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlpssretop  32388  finxpsuclem  32410  poimirlem31  32610  isbnd2  32752  bfplem2  32792  ghomco  32860  cnf1dd  33062  contrd  33069  mpt2bi123f  33141  mptbi12f  33145  jca2  33154  jca2r  33155  prter2  33184  lshpset2N  33424  cvrnbtwn2  33580  cvrnbtwn3  33581  cvrnbtwn4  33584  cvlcvr1  33644  hlrelat2  33707  cvrat4  33747  islpln2a  33852  linepsubN  34056  elpaddn0  34104  paddssw2  34148  pmapjoin  34156  ispsubcl2N  34251  dochkrshp  35693  dochsatshp  35758  mapdh9a  36097  hdmap11lem2  36152  pwinfi3  36887  rfovcnvf1od  37318  clsk1independent  37364  gneispace  37452  pm11.71  37619  sgoldbaltlem2  40202  uspgr2wlkeq  40854  setrec1lem4  42236
  Copyright terms: Public domain W3C validator