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  3847  domssl  8920  domssr  8921  sbthlem9  9008  nqerf  10821  lemul12a  11979  lediv12a  12015  elfzd  13415  fzass4  13462  4fvwrd4  13548  leexp1a  14082  wrd2ind  14630  cshwidxm1  14714  rtrclreclem4  14968  coprmproddvdslem  16573  reumodprminv  16716  prmgaplem6  16968  mreexexlem2d  17551  sgrp2nmndlem4  18836  pmtrrn2  19373  rngcinv  20553  ringcinv  20587  islmodd  20800  nn0srg  21375  rge0srg  21376  mdet1  22517  cpmatmcllem  22634  neitr  23096  restnlly  23398  llyrest  23401  llyidm  23404  uptx  23541  alexsubALTlem2  23964  alexsubALTlem4  23966  distspace  24232  ncvs1  25085  ivthlem3  25382  conway  27741  uzsind  28330  renegscl  28401  readdscl  28402  remulscl  28405  axtg5seg  28444  colperpexlem3  28711  outpasch  28734  iscgra1  28789  f1otrg  28850  ax5seg  28917  axcontlem4  28946  eengtrkg  28965  wlkonwlk1l  29641  crctcshwlkn0  29800  wwlksnextinj  29878  wwlksnextsurj  29879  clwwlkf1  30027  clwwlknon1  30075  numclwwlk1lem2f1  30335  wlkl0  30345  grpoidinv  30486  pjnmopi  32126  cdj1i  32411  xrofsup  32748  ccfldsrarelvec  33682  dya2iocnrect  34292  omssubadd  34311  sitgfval  34352  bnj969  34956  bnj1463  35065  erdszelem7  35239  rellysconn  35293  segconeq  36050  ifscgr  36084  btwnconn1lem13  36139  btwnconn1lem14  36140  outsideofeq  36170  ellines  36192  fnessref  36397  refssfne  36398  knoppndvlem14  36565  isbasisrelowllem1  37395  isbasisrelowllem2  37396  relowlssretop  37403  itg2gt0cn  37721  frinfm  37781  heiborlem3  37859  isfldidl  38114  4atlem12  39657  cdleme48fv  40544  cdlemg35  40758  mapd0  41710  aks4d1p1p5  42114  flt4lem7  42698  nna4b4nsq  42699  3cubeslem1  42723  mzpincl  42773  mzpindd  42785  diophin  42811  pellexlem3  42870  pellexlem5  42872  dfno2  43467  amgm3d  44238  amgm4d  44239  lptre2pt  45684  dvnprodlem2  45991  stoweidlem1  46045  stoweidlem14  46058  stoweidlem17  46061  stoweidlem27  46071  stoweidlem57  46101  fourierdlem12  46163  fourierdlem14  46165  fourierdlem70  46220  fourierdlem92  46242  fourierdlem111  46261  etransclem10  46288  etransclem24  46302  salgenval  46365  smfaddlem1  46807  f1cof1blem  47111  elfzelfzlble  47358  reuopreuprim  47563  gpgedgvtx0  48098  rngcinvALTV  48313  ringcinvALTV  48347  lmod1  48530  inlinecirc02plem  48824  nelsubclem  49105  oppf1st2nd  49169