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

Theorem jca32 559
 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 555 . 2 (𝜑 → (𝜒𝜃))
51, 4jca 555 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  1471  sbthlem9  8235  nqerf  9936  lemul12a  11065  lediv12a  11100  fzass4  12564  4fvwrd4  12645  leexp1a  13105  wrd2ind  13669  cshwidxm1  13745  rtrclreclem4  13992  coprmproddvdslem  15570  prmgaplem6  15954  mreexexlem2d  16499  sgrp2nmndlem4  17608  pmtrrn2  18072  islmodd  19063  nn0srg  20010  rge0srg  20011  mdet1  20601  cpmatmcllem  20717  neitr  21178  restnlly  21479  llyrest  21482  llyidm  21485  uptx  21622  alexsubALTlem2  22045  alexsubALTlem4  22047  distspace  22314  ncvs1  23149  ivthlem3  23414  axtg5seg  25555  colperpexlem3  25815  outpasch  25838  iscgra1  25893  f1otrg  25942  ax5seg  26009  axcontlem4  26038  eengtrkg  26056  wlkonwlk1l  26761  crctcshwlkn0  26916  wwlksnextinj  27009  wwlksnextsur  27010  clwwlkf1  27170  clwwlknon1  27237  numclwlk1lem2f1  27508  wlkl0  27520  grpoidinv  27663  pjnmopi  29308  cdj1i  29593  xrofsup  29834  dya2iocnrect  30644  omssubadd  30663  sitgfval  30704  bnj969  31315  bnj1463  31422  erdszelem7  31478  rellysconn  31532  conway  32208  etasslt  32218  segconeq  32415  ifscgr  32449  btwnconn1lem13  32504  btwnconn1lem14  32505  outsideofeq  32535  ellines  32557  fnessref  32650  refssfne  32651  knoppndvlem14  32814  isbasisrelowllem1  33506  isbasisrelowllem2  33507  relowlssretop  33514  itg2gt0cn  33770  frinfm  33835  heiborlem3  33917  isfldidl  34172  4atlem12  35393  cdleme48fv  36281  cdlemg35  36495  mapd0  37448  mzpincl  37791  mzpindd  37803  diophin  37830  pellexlem3  37889  pellexlem5  37891  amgm3d  38996  amgm4d  38997  monoords  40002  uzfissfz  40032  iuneqfzuzlem  40040  ssuzfz  40055  elfzd  40126  mccllem  40324  sumnnodd  40357  lptre2pt  40367  dvnmul  40653  dvnprodlem1  40656  dvnprodlem2  40657  itgspltprt  40690  stoweidlem1  40713  stoweidlem3  40715  stoweidlem14  40726  stoweidlem17  40729  stoweidlem27  40739  stoweidlem57  40769  fourierdlem12  40831  fourierdlem14  40833  fourierdlem41  40860  fourierdlem48  40866  fourierdlem49  40867  fourierdlem50  40868  fourierdlem70  40888  fourierdlem79  40897  fourierdlem92  40910  fourierdlem111  40929  elaa2lem  40945  etransclem3  40949  etransclem7  40953  etransclem10  40956  etransclem24  40970  etransclem27  40973  etransclem28  40974  etransclem35  40981  etransclem38  40984  etransclem44  40990  salgenval  41036  iundjiun  41172  caratheodorylem1  41238  smfaddlem1  41469  reuan  41678  elfzelfzlble  41833  rngcinv  42483  rngcinvALTV  42495  ringcinv  42534  lmod1  42783
 Copyright terms: Public domain W3C validator