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

Theorem jca32 507
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 503 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 503 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 198  df-an 385
This theorem is referenced by:  syl12anc  856  sbthlem9  8317  nqerf  10037  lemul12a  11166  lediv12a  11201  fzass4  12602  4fvwrd4  12683  leexp1a  13142  wrd2ind  13701  cshwidxm1  13777  rtrclreclem4  14024  coprmproddvdslem  15594  prmgaplem6  15977  mreexexlem2d  16510  sgrp2nmndlem4  17620  pmtrrn2  18081  islmodd  19073  nn0srg  20024  rge0srg  20025  mdet1  20618  cpmatmcllem  20736  neitr  21198  restnlly  21499  llyrest  21502  llyidm  21505  uptx  21642  alexsubALTlem2  22065  alexsubALTlem4  22067  distspace  22334  ncvs1  23169  ivthlem3  23434  axtg5seg  25578  colperpexlem3  25838  outpasch  25861  iscgra1  25916  f1otrg  25965  ax5seg  26032  axcontlem4  26061  eengtrkg  26079  wlkonwlk1l  26787  crctcshwlkn0  26942  wwlksnextinj  27036  wwlksnextsur  27037  clwwlkf1  27198  clwwlknon1  27265  numclwwlk1lem2f1  27536  wlkl0  27547  grpoidinv  27691  pjnmopi  29335  cdj1i  29620  xrofsup  29860  dya2iocnrect  30668  omssubadd  30687  sitgfval  30728  bnj969  31339  bnj1463  31446  erdszelem7  31502  rellysconn  31556  conway  32231  etasslt  32241  segconeq  32438  ifscgr  32472  btwnconn1lem13  32527  btwnconn1lem14  32528  outsideofeq  32558  ellines  32580  fnessref  32673  refssfne  32674  knoppndvlem14  32833  isbasisrelowllem1  33519  isbasisrelowllem2  33520  relowlssretop  33527  itg2gt0cn  33777  frinfm  33842  heiborlem3  33923  isfldidl  34178  4atlem12  35392  cdleme48fv  36280  cdlemg35  36494  mapd0  37446  mzpincl  37799  mzpindd  37811  diophin  37838  pellexlem3  37897  pellexlem5  37899  amgm3d  39002  amgm4d  39003  monoords  39992  uzfissfz  40022  iuneqfzuzlem  40030  ssuzfz  40045  elfzd  40115  mccllem  40309  sumnnodd  40342  lptre2pt  40352  dvnmul  40638  dvnprodlem1  40641  dvnprodlem2  40642  itgspltprt  40674  stoweidlem1  40697  stoweidlem3  40699  stoweidlem14  40710  stoweidlem17  40713  stoweidlem27  40723  stoweidlem57  40753  fourierdlem12  40815  fourierdlem14  40817  fourierdlem41  40844  fourierdlem48  40850  fourierdlem49  40851  fourierdlem50  40852  fourierdlem70  40872  fourierdlem79  40881  fourierdlem92  40894  fourierdlem111  40913  elaa2lem  40929  etransclem3  40933  etransclem7  40937  etransclem10  40940  etransclem24  40954  etransclem27  40957  etransclem28  40958  etransclem35  40965  etransclem38  40968  etransclem44  40974  salgenval  41020  iundjiun  41156  caratheodorylem1  41222  smfaddlem1  41453  reuan  41692  elfzelfzlble  41906  rngcinv  42549  rngcinvALTV  42561  ringcinv  42600  lmod1  42849
  Copyright terms: Public domain W3C validator