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  3859  domssl  8969  domssr  8970  sbthlem9  9059  nqerf  10883  lemul12a  12040  lediv12a  12076  elfzd  13476  fzass4  13523  4fvwrd4  13609  leexp1a  14140  wrd2ind  14688  cshwidxm1  14772  rtrclreclem4  15027  coprmproddvdslem  16632  reumodprminv  16775  prmgaplem6  17027  mreexexlem2d  17606  sgrp2nmndlem4  18855  pmtrrn2  19390  rngcinv  20546  ringcinv  20580  islmodd  20772  nn0srg  21354  rge0srg  21355  mdet1  22488  cpmatmcllem  22605  neitr  23067  restnlly  23369  llyrest  23372  llyidm  23375  uptx  23512  alexsubALTlem2  23935  alexsubALTlem4  23937  distspace  24204  ncvs1  25057  ivthlem3  25354  conway  27711  uzsind  28293  renegscl  28349  readdscl  28350  remulscl  28353  axtg5seg  28392  colperpexlem3  28659  outpasch  28682  iscgra1  28737  f1otrg  28798  ax5seg  28865  axcontlem4  28894  eengtrkg  28913  wlkonwlk1l  29591  crctcshwlkn0  29751  wwlksnextinj  29829  wwlksnextsurj  29830  clwwlkf1  29978  clwwlknon1  30026  numclwwlk1lem2f1  30286  wlkl0  30296  grpoidinv  30437  pjnmopi  32077  cdj1i  32362  xrofsup  32690  ccfldsrarelvec  33666  dya2iocnrect  34272  omssubadd  34291  sitgfval  34332  bnj969  34936  bnj1463  35045  erdszelem7  35184  rellysconn  35238  segconeq  35998  ifscgr  36032  btwnconn1lem13  36087  btwnconn1lem14  36088  outsideofeq  36118  ellines  36140  fnessref  36345  refssfne  36346  knoppndvlem14  36513  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  itg2gt0cn  37669  frinfm  37729  heiborlem3  37807  isfldidl  38062  4atlem12  39606  cdleme48fv  40493  cdlemg35  40707  mapd0  41659  aks4d1p1p5  42063  flt4lem7  42647  nna4b4nsq  42648  3cubeslem1  42672  mzpincl  42722  mzpindd  42734  diophin  42760  pellexlem3  42819  pellexlem5  42821  dfno2  43417  amgm3d  44188  amgm4d  44189  lptre2pt  45638  dvnprodlem2  45945  stoweidlem1  45999  stoweidlem14  46012  stoweidlem17  46015  stoweidlem27  46025  stoweidlem57  46055  fourierdlem12  46117  fourierdlem14  46119  fourierdlem70  46174  fourierdlem92  46196  fourierdlem111  46215  etransclem10  46242  etransclem24  46256  salgenval  46319  smfaddlem1  46761  f1cof1blem  47075  elfzelfzlble  47322  reuopreuprim  47527  gpgedgvtx0  48052  rngcinvALTV  48264  ringcinvALTV  48298  lmod1  48481  inlinecirc02plem  48775  nelsubclem  49056  oppf1st2nd  49120