Theorem jca32 516

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 512	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 512	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  reuan  3855  domssl  8945  domssr  8946  sbthlem9  9042  nqerf  10875  lemul12a  12022  lediv12a  12057  elfzd  13442  fzass4  13489  4fvwrd4  13571  leexp1a  14090  wrd2ind  14623  cshwidxm1  14707  rtrclreclem4  14958  coprmproddvdslem  16549  reumodprminv  16687  prmgaplem6  16939  mreexexlem2d  17539  sgrp2nmndlem4  18752  pmtrrn2  19256  islmodd  20384  nn0srg  20904  rge0srg  20905  mdet1  21987  cpmatmcllem  22104  neitr  22568  restnlly  22870  llyrest  22873  llyidm  22876  uptx  23013  alexsubALTlem2  23436  alexsubALTlem4  23438  distspace  23706  ncvs1  24558  ivthlem3  24854  conway  27181  axtg5seg  27470  colperpexlem3  27737  outpasch  27760  iscgra1  27815  f1otrg  27876  ax5seg  27950  axcontlem4  27979  eengtrkg  27998  wlkonwlk1l  28674  crctcshwlkn0  28829  wwlksnextinj  28907  wwlksnextsurj  28908  clwwlkf1  29056  clwwlknon1  29104  numclwwlk1lem2f1  29364  wlkl0  29374  grpoidinv  29513  pjnmopi  31153  cdj1i  31438  xrofsup  31740  ccfldsrarelvec  32442  dya2iocnrect  32970  omssubadd  32989  sitgfval  33030  bnj969  33647  bnj1463  33756  erdszelem7  33878  rellysconn  33932  segconeq  34671  ifscgr  34705  btwnconn1lem13  34760  btwnconn1lem14  34761  outsideofeq  34791  ellines  34813  fnessref  34905  refssfne  34906  knoppndvlem14  35064  isbasisrelowllem1  35899  isbasisrelowllem2  35900  relowlssretop  35907  itg2gt0cn  36206  frinfm  36267  heiborlem3  36345  isfldidl  36600  4atlem12  38148  cdleme48fv  39035  cdlemg35  39249  mapd0  40201  leexp1ad  40502  aks4d1p1p5  40605  flt4lem7  41055  nna4b4nsq  41056  3cubeslem1  41065  mzpincl  41115  mzpindd  41127  diophin  41153  pellexlem3  41212  pellexlem5  41214  dfno2  41822  amgm3d  42594  amgm4d  42595  lptre2pt  44001  dvnprodlem2  44308  stoweidlem1  44362  stoweidlem14  44375  stoweidlem17  44378  stoweidlem27  44388  stoweidlem57  44418  fourierdlem12  44480  fourierdlem14  44482  fourierdlem70  44537  fourierdlem92  44559  fourierdlem111  44578  etransclem10  44605  etransclem24  44619  salgenval  44682  smfaddlem1  45124  f1cof1blem  45428  elfzelfzlble  45673  reuopreuprim  45838  rngcinv  46399  rngcinvALTV  46411  ringcinv  46450  ringcinvALTV  46474  lmod1  46693  inlinecirc02plem  46992