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  3896  domssl  9038  domssr  9039  sbthlem9  9131  nqerf  10970  lemul12a  12125  lediv12a  12161  elfzd  13555  fzass4  13602  4fvwrd4  13688  leexp1a  14215  wrd2ind  14761  cshwidxm1  14845  rtrclreclem4  15100  coprmproddvdslem  16699  reumodprminv  16842  prmgaplem6  17094  mreexexlem2d  17688  sgrp2nmndlem4  18941  pmtrrn2  19478  rngcinv  20637  ringcinv  20671  islmodd  20864  nn0srg  21455  rge0srg  21456  mdet1  22607  cpmatmcllem  22724  neitr  23188  restnlly  23490  llyrest  23493  llyidm  23496  uptx  23633  alexsubALTlem2  24056  alexsubALTlem4  24058  distspace  24326  ncvs1  25191  ivthlem3  25488  conway  27844  uzsind  28391  renegscl  28430  readdscl  28431  remulscl  28434  axtg5seg  28473  colperpexlem3  28740  outpasch  28763  iscgra1  28818  f1otrg  28879  ax5seg  28953  axcontlem4  28982  eengtrkg  29001  wlkonwlk1l  29681  crctcshwlkn0  29841  wwlksnextinj  29919  wwlksnextsurj  29920  clwwlkf1  30068  clwwlknon1  30116  numclwwlk1lem2f1  30376  wlkl0  30386  grpoidinv  30527  pjnmopi  32167  cdj1i  32452  xrofsup  32771  ccfldsrarelvec  33721  dya2iocnrect  34283  omssubadd  34302  sitgfval  34343  bnj969  34960  bnj1463  35069  erdszelem7  35202  rellysconn  35256  segconeq  36011  ifscgr  36045  btwnconn1lem13  36100  btwnconn1lem14  36101  outsideofeq  36131  ellines  36153  fnessref  36358  refssfne  36359  knoppndvlem14  36526  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlssretop  37364  itg2gt0cn  37682  frinfm  37742  heiborlem3  37820  isfldidl  38075  4atlem12  39614  cdleme48fv  40501  cdlemg35  40715  mapd0  41667  leexp1ad  41973  aks4d1p1p5  42076  flt4lem7  42669  nna4b4nsq  42670  3cubeslem1  42695  mzpincl  42745  mzpindd  42757  diophin  42783  pellexlem3  42842  pellexlem5  42844  dfno2  43441  amgm3d  44212  amgm4d  44213  lptre2pt  45655  dvnprodlem2  45962  stoweidlem1  46016  stoweidlem14  46029  stoweidlem17  46032  stoweidlem27  46042  stoweidlem57  46072  fourierdlem12  46134  fourierdlem14  46136  fourierdlem70  46191  fourierdlem92  46213  fourierdlem111  46232  etransclem10  46259  etransclem24  46273  salgenval  46336  smfaddlem1  46778  f1cof1blem  47086  elfzelfzlble  47333  reuopreuprim  47513  gpgedgvtx0  48019  rngcinvALTV  48192  ringcinvALTV  48226  lmod1  48409  inlinecirc02plem  48707