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

Theorem jca32 557
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 554 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 554 1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  syl12anc  1321  sbthlem9  8022  nqerf  9696  lemul12a  10825  lediv12a  10860  fzass4  12321  elfz1b  12351  4fvwrd4  12400  leexp1a  12859  wrd2ind  13415  cshwidxm1  13490  rtrclreclem4  13735  coprmproddvdslem  15300  prmgaplem6  15684  mreexexlem2d  16226  sgrp2nmndlem4  17336  pmtrrn2  17801  islmodd  18790  nn0srg  19735  rge0srg  19736  mdet1  20326  cpmatmcllem  20442  neitr  20894  restnlly  21195  llyrest  21198  llyidm  21201  uptx  21338  alexsubALTlem2  21762  alexsubALTlem4  21764  distspace  22031  ncvs1  22865  ivthlem3  23129  axtg5seg  25264  colperpexlem3  25524  outpasch  25547  iscgra1  25602  f1otrg  25651  ax5seg  25718  axcontlem4  25747  eengtrkg  25765  wlkonwlk1l  26428  crctcshwlkn0  26582  wwlksnextinj  26663  wwlksnextsur  26664  clwwlksf1  26783  fusgr2wsp2nb  27056  grpoidinv  27208  pjnmopi  28853  cdj1i  29138  xrofsup  29374  dya2iocnrect  30121  omssubadd  30140  sitgfval  30181  bnj969  30721  bnj1463  30828  erdszelem7  30884  rellysconn  30938  segconeq  31756  ifscgr  31790  btwnconn1lem13  31845  btwnconn1lem14  31846  outsideofeq  31876  ellines  31898  fnessref  31991  refssfne  31992  knoppndvlem14  32155  isbasisrelowllem1  32832  isbasisrelowllem2  32833  relowlssretop  32840  itg2gt0cn  33094  frinfm  33159  heiborlem3  33241  isfldidl  33496  4atlem12  34375  cdleme48fv  35264  cdlemg35  35478  mapd0  36431  mzpincl  36774  mzpindd  36786  diophin  36813  pellexlem3  36872  pellexlem5  36874  amgm3d  37981  amgm4d  37982  monoords  38972  uzfissfz  39003  iuneqfzuzlem  39011  ssuzfz  39026  elfzd  39097  mccllem  39230  sumnnodd  39263  lptre2pt  39273  dvnmul  39461  dvnprodlem1  39464  dvnprodlem2  39465  itgspltprt  39499  stoweidlem1  39522  stoweidlem3  39524  stoweidlem14  39535  stoweidlem17  39538  stoweidlem27  39548  stoweidlem57  39578  fourierdlem12  39640  fourierdlem14  39642  fourierdlem41  39669  fourierdlem48  39675  fourierdlem49  39676  fourierdlem50  39677  fourierdlem70  39697  fourierdlem79  39706  fourierdlem92  39719  fourierdlem111  39738  elaa2lem  39754  etransclem3  39758  etransclem7  39762  etransclem10  39765  etransclem24  39779  etransclem27  39782  etransclem28  39783  etransclem35  39790  etransclem38  39793  etransclem44  39799  salgenval  39845  iundjiun  39981  caratheodorylem1  40044  smfaddlem1  40275  reuan  40481  elfzelfzlble  40625  rngcinv  41266  rngcinvALTV  41278  ringcinv  41317  lmod1  41566
  Copyright terms: Public domain W3C validator