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  3904  domssl  9036  domssr  9037  sbthlem9  9129  nqerf  10967  lemul12a  12122  lediv12a  12158  elfzd  13551  fzass4  13598  4fvwrd4  13684  leexp1a  14211  wrd2ind  14757  cshwidxm1  14841  rtrclreclem4  15096  coprmproddvdslem  16695  reumodprminv  16837  prmgaplem6  17089  mreexexlem2d  17689  sgrp2nmndlem4  18953  pmtrrn2  19492  rngcinv  20653  ringcinv  20687  islmodd  20880  nn0srg  21472  rge0srg  21473  mdet1  22622  cpmatmcllem  22739  neitr  23203  restnlly  23505  llyrest  23508  llyidm  23511  uptx  23648  alexsubALTlem2  24071  alexsubALTlem4  24073  distspace  24341  ncvs1  25204  ivthlem3  25501  conway  27858  uzsind  28405  renegscl  28444  readdscl  28445  remulscl  28448  axtg5seg  28487  colperpexlem3  28754  outpasch  28777  iscgra1  28832  f1otrg  28893  ax5seg  28967  axcontlem4  28996  eengtrkg  29015  wlkonwlk1l  29695  crctcshwlkn0  29850  wwlksnextinj  29928  wwlksnextsurj  29929  clwwlkf1  30077  clwwlknon1  30125  numclwwlk1lem2f1  30385  wlkl0  30395  grpoidinv  30536  pjnmopi  32176  cdj1i  32461  xrofsup  32777  ccfldsrarelvec  33695  dya2iocnrect  34262  omssubadd  34281  sitgfval  34322  bnj969  34938  bnj1463  35047  erdszelem7  35181  rellysconn  35235  segconeq  35991  ifscgr  36025  btwnconn1lem13  36080  btwnconn1lem14  36081  outsideofeq  36111  ellines  36133  fnessref  36339  refssfne  36340  knoppndvlem14  36507  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlssretop  37345  itg2gt0cn  37661  frinfm  37721  heiborlem3  37799  isfldidl  38054  4atlem12  39594  cdleme48fv  40481  cdlemg35  40695  mapd0  41647  leexp1ad  41953  aks4d1p1p5  42056  flt4lem7  42645  nna4b4nsq  42646  3cubeslem1  42671  mzpincl  42721  mzpindd  42733  diophin  42759  pellexlem3  42818  pellexlem5  42820  dfno2  43417  amgm3d  44188  amgm4d  44189  lptre2pt  45595  dvnprodlem2  45902  stoweidlem1  45956  stoweidlem14  45969  stoweidlem17  45972  stoweidlem27  45982  stoweidlem57  46012  fourierdlem12  46074  fourierdlem14  46076  fourierdlem70  46131  fourierdlem92  46153  fourierdlem111  46172  etransclem10  46199  etransclem24  46213  salgenval  46276  smfaddlem1  46718  f1cof1blem  47023  elfzelfzlble  47270  reuopreuprim  47450  gpgedgvtx0  47953  rngcinvALTV  48119  ringcinvALTV  48153  lmod1  48337  inlinecirc02plem  48635