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  3843  domssl  8929  domssr  8930  sbthlem9  9017  nqerf  10830  lemul12a  11988  lediv12a  12024  elfzd  13419  fzass4  13466  4fvwrd4  13552  leexp1a  14086  wrd2ind  14634  cshwidxm1  14718  rtrclreclem4  14972  coprmproddvdslem  16577  reumodprminv  16720  prmgaplem6  16972  mreexexlem2d  17555  sgrp2nmndlem4  18840  pmtrrn2  19376  rngcinv  20556  ringcinv  20590  islmodd  20803  nn0srg  21378  rge0srg  21379  mdet1  22519  cpmatmcllem  22636  neitr  23098  restnlly  23400  llyrest  23403  llyidm  23406  uptx  23543  alexsubALTlem2  23966  alexsubALTlem4  23968  distspace  24234  ncvs1  25087  ivthlem3  25384  conway  27743  uzsind  28332  renegscl  28403  readdscl  28404  remulscl  28407  axtg5seg  28446  colperpexlem3  28713  outpasch  28736  iscgra1  28791  f1otrg  28852  ax5seg  28920  axcontlem4  28949  eengtrkg  28968  wlkonwlk1l  29644  crctcshwlkn0  29803  wwlksnextinj  29881  wwlksnextsurj  29882  clwwlkf1  30033  clwwlknon1  30081  numclwwlk1lem2f1  30341  wlkl0  30351  grpoidinv  30492  pjnmopi  32132  cdj1i  32417  xrofsup  32756  ccfldsrarelvec  33707  dya2iocnrect  34317  omssubadd  34336  sitgfval  34377  bnj969  34981  bnj1463  35090  erdszelem7  35264  rellysconn  35318  segconeq  36077  ifscgr  36111  btwnconn1lem13  36166  btwnconn1lem14  36167  outsideofeq  36197  ellines  36219  fnessref  36424  refssfne  36425  knoppndvlem14  36592  isbasisrelowllem1  37422  isbasisrelowllem2  37423  relowlssretop  37430  itg2gt0cn  37738  frinfm  37798  heiborlem3  37876  isfldidl  38131  4atlem12  39734  cdleme48fv  40621  cdlemg35  40835  mapd0  41787  aks4d1p1p5  42191  flt4lem7  42780  nna4b4nsq  42781  3cubeslem1  42804  mzpincl  42854  mzpindd  42866  diophin  42892  pellexlem3  42951  pellexlem5  42953  dfno2  43548  amgm3d  44319  amgm4d  44320  lptre2pt  45765  dvnprodlem2  46072  stoweidlem1  46126  stoweidlem14  46139  stoweidlem17  46142  stoweidlem27  46152  stoweidlem57  46182  fourierdlem12  46244  fourierdlem14  46246  fourierdlem70  46301  fourierdlem92  46323  fourierdlem111  46342  etransclem10  46369  etransclem24  46383  salgenval  46446  smfaddlem1  46888  f1cof1blem  47201  elfzelfzlble  47448  reuopreuprim  47653  gpgedgvtx0  48188  rngcinvALTV  48403  ringcinvALTV  48437  lmod1  48620  inlinecirc02plem  48914  nelsubclem  49195  oppf1st2nd  49259