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

Theorem jca32 519
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 515 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 515 1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  reuan  3828  sbthlem9  8623  nqerf  10345  lemul12a  11491  lediv12a  11526  elfzd  12897  fzass4  12944  4fvwrd4  13026  leexp1a  13539  wrd2ind  14080  cshwidxm1  14164  rtrclreclem4  14416  coprmproddvdslem  16000  reumodprminv  16135  prmgaplem6  16386  mreexexlem2d  16912  sgrp2nmndlem4  18089  pmtrrn2  18584  islmodd  19637  nn0srg  20165  rge0srg  20166  mdet1  21210  cpmatmcllem  21327  neitr  21789  restnlly  22091  llyrest  22094  llyidm  22097  uptx  22234  alexsubALTlem2  22657  alexsubALTlem4  22659  distspace  22927  ncvs1  23766  ivthlem3  24061  axtg5seg  26263  colperpexlem3  26530  outpasch  26553  iscgra1  26608  f1otrg  26669  ax5seg  26736  axcontlem4  26765  eengtrkg  26784  wlkonwlk1l  27457  crctcshwlkn0  27611  wwlksnextinj  27689  wwlksnextsurj  27690  clwwlkf1  27838  clwwlknon1  27886  numclwwlk1lem2f1  28146  wlkl0  28156  grpoidinv  28295  pjnmopi  29935  cdj1i  30220  xrofsup  30522  ccfldsrarelvec  31148  dya2iocnrect  31653  omssubadd  31672  sitgfval  31713  bnj969  32332  bnj1463  32441  erdszelem7  32558  rellysconn  32612  conway  33378  etasslt  33388  segconeq  33585  ifscgr  33619  btwnconn1lem13  33674  btwnconn1lem14  33675  outsideofeq  33705  ellines  33727  fnessref  33819  refssfne  33820  knoppndvlem14  33978  isbasisrelowllem1  34773  isbasisrelowllem2  34774  relowlssretop  34781  itg2gt0cn  35111  frinfm  35172  heiborlem3  35250  isfldidl  35505  4atlem12  36907  cdleme48fv  37794  cdlemg35  38008  mapd0  38960  leexp1ad  39257  3cubeslem1  39618  mzpincl  39668  mzpindd  39680  diophin  39706  pellexlem3  39765  pellexlem5  39767  amgm3d  40898  amgm4d  40899  monoords  41922  uzfissfz  41951  iuneqfzuzlem  41959  ssuzfz  41974  mccllem  42232  sumnnodd  42265  lptre2pt  42275  dvnmul  42578  dvnprodlem1  42581  dvnprodlem2  42582  itgspltprt  42614  stoweidlem1  42636  stoweidlem3  42638  stoweidlem14  42649  stoweidlem17  42652  stoweidlem27  42662  stoweidlem57  42692  fourierdlem12  42754  fourierdlem14  42756  fourierdlem41  42783  fourierdlem48  42789  fourierdlem49  42790  fourierdlem50  42791  fourierdlem70  42811  fourierdlem79  42820  fourierdlem92  42833  fourierdlem111  42852  elaa2lem  42868  etransclem3  42872  etransclem7  42876  etransclem10  42879  etransclem24  42893  etransclem27  42896  etransclem28  42897  etransclem35  42904  etransclem38  42907  etransclem44  42913  salgenval  42956  iundjiun  43092  caratheodorylem1  43158  smfaddlem1  43389  elfzelfzlble  43871  reuopreuprim  44036  rngcinv  44598  rngcinvALTV  44610  ringcinv  44649  lmod1  44894  inlinecirc02plem  45193
  Copyright terms: Public domain W3C validator