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

Theorem jca32 517
Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1 (𝜑𝜓)
jca31.2 (𝜑𝜒)
jca31.3 (𝜑𝜃)
Assertion
Ref Expression
jca32 (𝜑 → (𝜓 ∧ (𝜒𝜃)))

Proof of Theorem jca32
StepHypRef Expression
1 jca31.1 . 2 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
3 jca31.3 . . 3 (𝜑𝜃)
42, 3jca 513 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 513 1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  reuan  3856  domssl  8944  domssr  8945  sbthlem9  9041  nqerf  10874  lemul12a  12021  lediv12a  12056  elfzd  13441  fzass4  13488  4fvwrd4  13570  leexp1a  14089  wrd2ind  14620  cshwidxm1  14704  rtrclreclem4  14955  coprmproddvdslem  16546  reumodprminv  16684  prmgaplem6  16936  mreexexlem2d  17533  sgrp2nmndlem4  18746  pmtrrn2  19250  islmodd  20371  nn0srg  20890  rge0srg  20891  mdet1  21973  cpmatmcllem  22090  neitr  22554  restnlly  22856  llyrest  22859  llyidm  22862  uptx  22999  alexsubALTlem2  23422  alexsubALTlem4  23424  distspace  23692  ncvs1  24544  ivthlem3  24840  conway  27167  axtg5seg  27456  colperpexlem3  27723  outpasch  27746  iscgra1  27801  f1otrg  27862  ax5seg  27936  axcontlem4  27965  eengtrkg  27984  wlkonwlk1l  28660  crctcshwlkn0  28815  wwlksnextinj  28893  wwlksnextsurj  28894  clwwlkf1  29042  clwwlknon1  29090  numclwwlk1lem2f1  29350  wlkl0  29360  grpoidinv  29499  pjnmopi  31139  cdj1i  31424  xrofsup  31726  ccfldsrarelvec  32419  dya2iocnrect  32945  omssubadd  32964  sitgfval  33005  bnj969  33622  bnj1463  33731  erdszelem7  33855  rellysconn  33909  segconeq  34648  ifscgr  34682  btwnconn1lem13  34737  btwnconn1lem14  34738  outsideofeq  34768  ellines  34790  fnessref  34882  refssfne  34883  knoppndvlem14  35041  isbasisrelowllem1  35876  isbasisrelowllem2  35877  relowlssretop  35884  itg2gt0cn  36183  frinfm  36244  heiborlem3  36322  isfldidl  36577  4atlem12  38125  cdleme48fv  39012  cdlemg35  39226  mapd0  40178  leexp1ad  40479  aks4d1p1p5  40582  flt4lem7  41044  nna4b4nsq  41045  3cubeslem1  41054  mzpincl  41104  mzpindd  41116  diophin  41142  pellexlem3  41201  pellexlem5  41203  dfno2  41792  amgm3d  42564  amgm4d  42565  lptre2pt  43971  dvnprodlem2  44278  stoweidlem1  44332  stoweidlem14  44345  stoweidlem17  44348  stoweidlem27  44358  stoweidlem57  44388  fourierdlem12  44450  fourierdlem14  44452  fourierdlem70  44507  fourierdlem92  44529  fourierdlem111  44548  etransclem10  44575  etransclem24  44589  salgenval  44652  smfaddlem1  45094  f1cof1blem  45398  elfzelfzlble  45643  reuopreuprim  45808  rngcinv  46369  rngcinvALTV  46381  ringcinv  46420  ringcinvALTV  46444  lmod1  46663  inlinecirc02plem  46962
  Copyright terms: Public domain W3C validator