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  3835  domssl  8938  domssr  8939  sbthlem9  9026  nqerf  10844  lemul12a  12004  lediv12a  12040  elfzd  13460  fzass4  13507  4fvwrd4  13593  leexp1a  14128  wrd2ind  14676  cshwidxm1  14760  rtrclreclem4  15014  coprmproddvdslem  16622  reumodprminv  16766  prmgaplem6  17018  mreexexlem2d  17602  sgrp2nmndlem4  18890  pmtrrn2  19426  rngcinv  20605  ringcinv  20639  islmodd  20852  nn0srg  21427  rge0srg  21428  mdet1  22576  cpmatmcllem  22693  neitr  23155  restnlly  23457  llyrest  23460  llyidm  23463  uptx  23600  alexsubALTlem2  24023  alexsubALTlem4  24025  distspace  24291  ncvs1  25134  ivthlem3  25430  conway  27785  uzsind  28411  renegscl  28504  readdscl  28505  remulscl  28508  axtg5seg  28547  colperpexlem3  28814  outpasch  28837  iscgra1  28892  f1otrg  28953  ax5seg  29021  axcontlem4  29050  eengtrkg  29069  wlkonwlk1l  29745  crctcshwlkn0  29904  wwlksnextinj  29982  wwlksnextsurj  29983  clwwlkf1  30134  clwwlknon1  30182  numclwwlk1lem2f1  30442  wlkl0  30452  grpoidinv  30594  pjnmopi  32234  cdj1i  32519  xrofsup  32855  ccfldsrarelvec  33831  dya2iocnrect  34441  omssubadd  34460  sitgfval  34501  bnj969  35104  bnj1463  35213  erdszelem7  35395  rellysconn  35449  segconeq  36208  ifscgr  36242  btwnconn1lem13  36297  btwnconn1lem14  36298  outsideofeq  36328  ellines  36350  fnessref  36555  refssfne  36556  knoppndvlem14  36801  isbasisrelowllem1  37685  isbasisrelowllem2  37686  relowlssretop  37693  itg2gt0cn  38010  frinfm  38070  heiborlem3  38148  isfldidl  38403  eldisjs6  39275  4atlem12  40072  cdleme48fv  40959  cdlemg35  41173  mapd0  42125  aks4d1p1p5  42528  flt4lem7  43106  nna4b4nsq  43107  3cubeslem1  43130  mzpincl  43180  mzpindd  43192  diophin  43218  pellexlem3  43277  pellexlem5  43279  dfno2  43873  amgm3d  44644  amgm4d  44645  lptre2pt  46086  dvnprodlem2  46393  stoweidlem1  46447  stoweidlem14  46460  stoweidlem17  46463  stoweidlem27  46473  stoweidlem57  46503  fourierdlem12  46565  fourierdlem14  46567  fourierdlem70  46622  fourierdlem92  46644  fourierdlem111  46663  etransclem10  46690  etransclem24  46704  salgenval  46767  smfaddlem1  47209  f1cof1blem  47534  elfzelfzlble  47781  reuopreuprim  47998  gpgedgvtx0  48549  rngcinvALTV  48764  ringcinvALTV  48798  lmod1  48980  inlinecirc02plem  49274  nelsubclem  49554  oppf1st2nd  49618