Theorem jca32 515

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

Step	Hyp	Ref	Expression
1		jca31.1	. 2 ⊢ (𝜑 → 𝜓)
2		jca31.2	. . 3 ⊢ (𝜑 → 𝜒)
3		jca31.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 511	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reuan  3846  domssl  8935  domssr  8936  sbthlem9  9023  nqerf  10841  lemul12a  11999  lediv12a  12035  elfzd  13431  fzass4  13478  4fvwrd4  13564  leexp1a  14098  wrd2ind  14646  cshwidxm1  14730  rtrclreclem4  14984  coprmproddvdslem  16589  reumodprminv  16732  prmgaplem6  16984  mreexexlem2d  17568  sgrp2nmndlem4  18853  pmtrrn2  19389  rngcinv  20570  ringcinv  20604  islmodd  20817  nn0srg  21392  rge0srg  21393  mdet1  22545  cpmatmcllem  22662  neitr  23124  restnlly  23426  llyrest  23429  llyidm  23432  uptx  23569  alexsubALTlem2  23992  alexsubALTlem4  23994  distspace  24260  ncvs1  25113  ivthlem3  25410  conway  27775  uzsind  28401  renegscl  28494  readdscl  28495  remulscl  28498  axtg5seg  28537  colperpexlem3  28804  outpasch  28827  iscgra1  28882  f1otrg  28943  ax5seg  29011  axcontlem4  29040  eengtrkg  29059  wlkonwlk1l  29735  crctcshwlkn0  29894  wwlksnextinj  29972  wwlksnextsurj  29973  clwwlkf1  30124  clwwlknon1  30172  numclwwlk1lem2f1  30432  wlkl0  30442  grpoidinv  30583  pjnmopi  32223  cdj1i  32508  xrofsup  32847  ccfldsrarelvec  33828  dya2iocnrect  34438  omssubadd  34457  sitgfval  34498  bnj969  35102  bnj1463  35211  erdszelem7  35391  rellysconn  35445  segconeq  36204  ifscgr  36238  btwnconn1lem13  36293  btwnconn1lem14  36294  outsideofeq  36324  ellines  36346  fnessref  36551  refssfne  36552  knoppndvlem14  36725  isbasisrelowllem1  37560  isbasisrelowllem2  37561  relowlssretop  37568  itg2gt0cn  37876  frinfm  37936  heiborlem3  38014  isfldidl  38269  4atlem12  39872  cdleme48fv  40759  cdlemg35  40973  mapd0  41925  aks4d1p1p5  42329  flt4lem7  42902  nna4b4nsq  42903  3cubeslem1  42926  mzpincl  42976  mzpindd  42988  diophin  43014  pellexlem3  43073  pellexlem5  43075  dfno2  43669  amgm3d  44440  amgm4d  44441  lptre2pt  45884  dvnprodlem2  46191  stoweidlem1  46245  stoweidlem14  46258  stoweidlem17  46261  stoweidlem27  46271  stoweidlem57  46301  fourierdlem12  46363  fourierdlem14  46365  fourierdlem70  46420  fourierdlem92  46442  fourierdlem111  46461  etransclem10  46488  etransclem24  46502  salgenval  46565  smfaddlem1  47007  f1cof1blem  47320  elfzelfzlble  47567  reuopreuprim  47772  gpgedgvtx0  48307  rngcinvALTV  48522  ringcinvALTV  48556  lmod1  48738  inlinecirc02plem  49032  nelsubclem  49312  oppf1st2nd  49376