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

Theorem jcad 513
Description: Deduction conjoining the consequents of two implications. Deduction form of jca 512 and double deduction form of pm3.2 470 and pm3.2i 471. (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 470 . 2 (𝜒 → (𝜃 → (𝜒𝜃)))
41, 2, 3syl6c 70 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  jca2  514  jctild  526  jctird  527  ancld  551  ancrd  552  oplem1  1050  2eu1  2734  2eu1OLD  2735  2eu1v  2736  disjxiun  5060  iss  5902  oneqmini  6241  funssres  6397  elpreima  6826  isomin  7084  oneqmin  7513  frxp  7816  tposfo2  7911  oa00  8180  odi  8200  oneo  8202  oeordsuc  8215  oelim2  8216  nnarcl  8237  nnmord  8253  nnneo  8273  map0g  8443  onomeneq  8702  pssnn  8730  fodomfib  8792  inf3lem4  9088  cplem1  9312  karden  9318  alephordi  9494  cardinfima  9517  dfac5lem5  9547  isf34lem4  9793  axcc4  9855  axdc3lem2  9867  zorn2lem4  9915  zorn2lem7  9918  indpi  10323  genpcl  10424  addclprlem2  10433  ltaddpr  10450  ltexprlem5  10456  suplem1pr  10468  ltlen  10735  dedekind  10797  mulgt1  11493  sup2  11591  nominpos  11868  uzind  12068  xrmaxlt  12569  xrltmin  12570  xrmaxle  12571  xrlemin  12572  xmullem2  12653  ccatopth  14073  shftuz  14423  sqreulem  14714  limsupbnd2  14835  mulcn2  14947  sadcaddlem  15801  dvdsgcdb  15888  algcvgblem  15916  lcmdvdsb  15952  rpexp  16059  infpnlem1  16241  divsfval  16815  iscatd  16939  posasymb  17557  plttr  17575  joinle  17619  meetle  17633  latnlej  17673  latnlej2  17676  lsmlub  18726  imasring  19305  unitmulclb  19351  lbspss  19790  lspsneu  19831  lspprat  19861  assapropd  20036  isclo2  21631  cncls2  21816  cncls  21817  cnntr  21818  cnrest2  21829  cmpsub  21943  cmpcld  21945  kgenss  22086  ptpjpre1  22114  txlm  22191  qtoptop2  22242  cmphaushmeo  22343  fbun  22383  isfild  22401  fbasrn  22427  fgtr  22433  ufinffr  22472  rnelfm  22496  fmfnfmlem4  22500  ghmcnp  22657  metrest  23068  icoopnst  23477  iocopnst  23478  dgreq0  24789  plyexmo  24836  cxpeq0  25193  mumullem2  25690  chpchtsum  25728  bposlem7  25799  lgsqr  25860  uspgr2wlkeq  27360  wwlknllvtx  27557  ex-natded5.3-2  28120  ubthlem1  28580  axhcompl-zf  28708  ococss  29003  nmopun  29724  elpjrn  29900  stm1addi  29955  stm1add3i  29957  mdsl1i  30031  chrelat2i  30075  atexch  30091  atcvat4i  30107  mdsymlem3  30115  bian1d  30157  bnj600  32096  subgrwlk  32282  pthacycspth  32307  subfacval2  32337  climuzcnv  32817  fundmpss  32912  soseq  32999  sltres  33072  nosupno  33106  segconeq  33374  ifscgr  33408  endofsegid  33449  colinbtwnle  33482  trer  33567  ivthALT  33586  fnessref  33608  fnemeet2  33618  fnejoin2  33620  onsuct0  33692  bj-ideqg1  34354  bj-elid6  34360  bj-finsumval0  34461  bj-isrvec2  34475  bj-bary1  34487  icorempo  34520  isbasisrelowllem1  34524  isbasisrelowllem2  34525  relowlpssretop  34533  finxpsuclem  34566  pibt2  34586  poimirlem31  34809  isbnd2  34948  bfplem2  34988  ghomco  35056  cnf1dd  35255  contrd  35262  mpobi123f  35327  mptbi12f  35331  iss2  35488  jca2r  35877  prter2  35903  lshpset2N  36141  cvrnbtwn2  36297  cvrnbtwn3  36298  cvrnbtwn4  36301  cvlcvr1  36361  hlrelat2  36425  cvrat4  36465  islpln2a  36570  linepsubN  36774  elpaddn0  36822  paddssw2  36866  pmapjoin  36874  ispsubcl2N  36969  dochkrshp  38408  dochsatshp  38473  mapdh9a  38811  hdmap11lem2  38864  frlmfzowrdb  39027  pwinfi3  39806  clsk1independent  40280  gneispace  40368  pm11.71  40613  2reu8i  43197  sbgoldbaltlem2  43796  setrec1lem4  44695
  Copyright terms: Public domain W3C validator