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 553 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 553 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 197  df-an 385
This theorem is referenced by:  syl12anc  1364  sbthlem9  8119  nqerf  9790  lemul12a  10919  lediv12a  10954  fzass4  12417  4fvwrd4  12498  leexp1a  12959  wrd2ind  13523  cshwidxm1  13599  rtrclreclem4  13845  coprmproddvdslem  15423  prmgaplem6  15807  mreexexlem2d  16352  sgrp2nmndlem4  17462  pmtrrn2  17926  islmodd  18917  nn0srg  19864  rge0srg  19865  mdet1  20455  cpmatmcllem  20571  neitr  21032  restnlly  21333  llyrest  21336  llyidm  21339  uptx  21476  alexsubALTlem2  21899  alexsubALTlem4  21901  distspace  22168  ncvs1  23003  ivthlem3  23268  axtg5seg  25409  colperpexlem3  25669  outpasch  25692  iscgra1  25747  f1otrg  25796  ax5seg  25863  axcontlem4  25892  eengtrkg  25910  wlkonwlk1l  26615  crctcshwlkn0  26769  wwlksnextinj  26862  wwlksnextsur  26863  clwwlkf1  27012  clwwlknon1  27072  numclwlk1lem2f1  27347  grpoidinv  27490  pjnmopi  29135  cdj1i  29420  xrofsup  29661  dya2iocnrect  30471  omssubadd  30490  sitgfval  30531  bnj969  31142  bnj1463  31249  erdszelem7  31305  rellysconn  31359  conway  32035  etasslt  32045  segconeq  32242  ifscgr  32276  btwnconn1lem13  32331  btwnconn1lem14  32332  outsideofeq  32362  ellines  32384  fnessref  32477  refssfne  32478  knoppndvlem14  32641  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlssretop  33341  itg2gt0cn  33595  frinfm  33660  heiborlem3  33742  isfldidl  33997  4atlem12  35216  cdleme48fv  36104  cdlemg35  36318  mapd0  37271  mzpincl  37614  mzpindd  37626  diophin  37653  pellexlem3  37712  pellexlem5  37714  amgm3d  38819  amgm4d  38820  monoords  39825  uzfissfz  39855  iuneqfzuzlem  39863  ssuzfz  39878  elfzd  39949  mccllem  40147  sumnnodd  40180  lptre2pt  40190  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  itgspltprt  40513  stoweidlem1  40536  stoweidlem3  40538  stoweidlem14  40549  stoweidlem17  40552  stoweidlem27  40562  stoweidlem57  40592  fourierdlem12  40654  fourierdlem14  40656  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem70  40711  fourierdlem79  40720  fourierdlem92  40733  fourierdlem111  40752  elaa2lem  40768  etransclem3  40772  etransclem7  40776  etransclem10  40779  etransclem24  40793  etransclem27  40796  etransclem28  40797  etransclem35  40804  etransclem38  40807  etransclem44  40813  salgenval  40859  iundjiun  40995  caratheodorylem1  41061  smfaddlem1  41292  reuan  41501  elfzelfzlble  41656  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  lmod1  42606
  Copyright terms: Public domain W3C validator