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  3871  domssl  9010  domssr  9011  sbthlem9  9103  nqerf  10942  lemul12a  12097  lediv12a  12133  elfzd  13530  fzass4  13577  4fvwrd4  13663  leexp1a  14191  wrd2ind  14739  cshwidxm1  14823  rtrclreclem4  15078  coprmproddvdslem  16679  reumodprminv  16822  prmgaplem6  17074  mreexexlem2d  17655  sgrp2nmndlem4  18904  pmtrrn2  19439  rngcinv  20595  ringcinv  20629  islmodd  20821  nn0srg  21403  rge0srg  21404  mdet1  22537  cpmatmcllem  22654  neitr  23116  restnlly  23418  llyrest  23421  llyidm  23424  uptx  23561  alexsubALTlem2  23984  alexsubALTlem4  23986  distspace  24253  ncvs1  25107  ivthlem3  25404  conway  27761  uzsind  28308  renegscl  28347  readdscl  28348  remulscl  28351  axtg5seg  28390  colperpexlem3  28657  outpasch  28680  iscgra1  28735  f1otrg  28796  ax5seg  28863  axcontlem4  28892  eengtrkg  28911  wlkonwlk1l  29589  crctcshwlkn0  29749  wwlksnextinj  29827  wwlksnextsurj  29828  clwwlkf1  29976  clwwlknon1  30024  numclwwlk1lem2f1  30284  wlkl0  30294  grpoidinv  30435  pjnmopi  32075  cdj1i  32360  xrofsup  32690  ccfldsrarelvec  33658  dya2iocnrect  34259  omssubadd  34278  sitgfval  34319  bnj969  34923  bnj1463  35032  erdszelem7  35165  rellysconn  35219  segconeq  35974  ifscgr  36008  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeq  36094  ellines  36116  fnessref  36321  refssfne  36322  knoppndvlem14  36489  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlssretop  37327  itg2gt0cn  37645  frinfm  37705  heiborlem3  37783  isfldidl  38038  4atlem12  39577  cdleme48fv  40464  cdlemg35  40678  mapd0  41630  aks4d1p1p5  42034  flt4lem7  42629  nna4b4nsq  42630  3cubeslem1  42654  mzpincl  42704  mzpindd  42716  diophin  42742  pellexlem3  42801  pellexlem5  42803  dfno2  43399  amgm3d  44170  amgm4d  44171  lptre2pt  45617  dvnprodlem2  45924  stoweidlem1  45978  stoweidlem14  45991  stoweidlem17  45994  stoweidlem27  46004  stoweidlem57  46034  fourierdlem12  46096  fourierdlem14  46098  fourierdlem70  46153  fourierdlem92  46175  fourierdlem111  46194  etransclem10  46221  etransclem24  46235  salgenval  46298  smfaddlem1  46740  f1cof1blem  47051  elfzelfzlble  47298  reuopreuprim  47488  gpgedgvtx0  48013  rngcinvALTV  48199  ringcinvALTV  48233  lmod1  48416  inlinecirc02plem  48714  nelsubclem  48982  oppf1st2nd  49027