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  3918  domssl  9058  domssr  9059  sbthlem9  9157  nqerf  10999  lemul12a  12152  lediv12a  12188  elfzd  13575  fzass4  13622  4fvwrd4  13705  leexp1a  14225  wrd2ind  14771  cshwidxm1  14855  rtrclreclem4  15110  coprmproddvdslem  16709  reumodprminv  16851  prmgaplem6  17103  mreexexlem2d  17703  sgrp2nmndlem4  18963  pmtrrn2  19502  rngcinv  20659  ringcinv  20693  islmodd  20886  nn0srg  21478  rge0srg  21479  mdet1  22628  cpmatmcllem  22745  neitr  23209  restnlly  23511  llyrest  23514  llyidm  23517  uptx  23654  alexsubALTlem2  24077  alexsubALTlem4  24079  distspace  24347  ncvs1  25210  ivthlem3  25507  conway  27862  uzsind  28409  renegscl  28448  readdscl  28449  remulscl  28452  axtg5seg  28491  colperpexlem3  28758  outpasch  28781  iscgra1  28836  f1otrg  28897  ax5seg  28971  axcontlem4  29000  eengtrkg  29019  wlkonwlk1l  29699  crctcshwlkn0  29854  wwlksnextinj  29932  wwlksnextsurj  29933  clwwlkf1  30081  clwwlknon1  30129  numclwwlk1lem2f1  30389  wlkl0  30399  grpoidinv  30540  pjnmopi  32180  cdj1i  32465  xrofsup  32774  ccfldsrarelvec  33681  dya2iocnrect  34246  omssubadd  34265  sitgfval  34306  bnj969  34922  bnj1463  35031  erdszelem7  35165  rellysconn  35219  segconeq  35974  ifscgr  36008  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeq  36094  ellines  36116  fnessref  36323  refssfne  36324  knoppndvlem14  36491  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  itg2gt0cn  37635  frinfm  37695  heiborlem3  37773  isfldidl  38028  4atlem12  39569  cdleme48fv  40456  cdlemg35  40670  mapd0  41622  leexp1ad  41928  aks4d1p1p5  42032  flt4lem7  42614  nna4b4nsq  42615  3cubeslem1  42640  mzpincl  42690  mzpindd  42702  diophin  42728  pellexlem3  42787  pellexlem5  42789  dfno2  43390  amgm3d  44161  amgm4d  44162  lptre2pt  45561  dvnprodlem2  45868  stoweidlem1  45922  stoweidlem14  45935  stoweidlem17  45938  stoweidlem27  45948  stoweidlem57  45978  fourierdlem12  46040  fourierdlem14  46042  fourierdlem70  46097  fourierdlem92  46119  fourierdlem111  46138  etransclem10  46165  etransclem24  46179  salgenval  46242  smfaddlem1  46684  f1cof1blem  46989  elfzelfzlble  47236  reuopreuprim  47400  rngcinvALTV  47999  ringcinvALTV  48033  lmod1  48221  inlinecirc02plem  48520