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  3856  domssl  8946  domssr  8947  sbthlem9  9036  nqerf  10859  lemul12a  12016  lediv12a  12052  elfzd  13452  fzass4  13499  4fvwrd4  13585  leexp1a  14116  wrd2ind  14664  cshwidxm1  14748  rtrclreclem4  15003  coprmproddvdslem  16608  reumodprminv  16751  prmgaplem6  17003  mreexexlem2d  17582  sgrp2nmndlem4  18831  pmtrrn2  19366  rngcinv  20522  ringcinv  20556  islmodd  20748  nn0srg  21330  rge0srg  21331  mdet1  22464  cpmatmcllem  22581  neitr  23043  restnlly  23345  llyrest  23348  llyidm  23351  uptx  23488  alexsubALTlem2  23911  alexsubALTlem4  23913  distspace  24180  ncvs1  25033  ivthlem3  25330  conway  27687  uzsind  28269  renegscl  28325  readdscl  28326  remulscl  28329  axtg5seg  28368  colperpexlem3  28635  outpasch  28658  iscgra1  28713  f1otrg  28774  ax5seg  28841  axcontlem4  28870  eengtrkg  28889  wlkonwlk1l  29565  crctcshwlkn0  29724  wwlksnextinj  29802  wwlksnextsurj  29803  clwwlkf1  29951  clwwlknon1  29999  numclwwlk1lem2f1  30259  wlkl0  30269  grpoidinv  30410  pjnmopi  32050  cdj1i  32335  xrofsup  32663  ccfldsrarelvec  33639  dya2iocnrect  34245  omssubadd  34264  sitgfval  34305  bnj969  34909  bnj1463  35018  erdszelem7  35157  rellysconn  35211  segconeq  35971  ifscgr  36005  btwnconn1lem13  36060  btwnconn1lem14  36061  outsideofeq  36091  ellines  36113  fnessref  36318  refssfne  36319  knoppndvlem14  36486  isbasisrelowllem1  37316  isbasisrelowllem2  37317  relowlssretop  37324  itg2gt0cn  37642  frinfm  37702  heiborlem3  37780  isfldidl  38035  4atlem12  39579  cdleme48fv  40466  cdlemg35  40680  mapd0  41632  aks4d1p1p5  42036  flt4lem7  42620  nna4b4nsq  42621  3cubeslem1  42645  mzpincl  42695  mzpindd  42707  diophin  42733  pellexlem3  42792  pellexlem5  42794  dfno2  43390  amgm3d  44161  amgm4d  44162  lptre2pt  45611  dvnprodlem2  45918  stoweidlem1  45972  stoweidlem14  45985  stoweidlem17  45988  stoweidlem27  45998  stoweidlem57  46028  fourierdlem12  46090  fourierdlem14  46092  fourierdlem70  46147  fourierdlem92  46169  fourierdlem111  46188  etransclem10  46215  etransclem24  46229  salgenval  46292  smfaddlem1  46734  f1cof1blem  47048  elfzelfzlble  47295  reuopreuprim  47500  gpgedgvtx0  48025  rngcinvALTV  48237  ringcinvALTV  48271  lmod1  48454  inlinecirc02plem  48748  nelsubclem  49029  oppf1st2nd  49093