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 206  df-an 396

This theorem is referenced by:  reuan  3825  sbthlem9  8831  nqerf  10617  lemul12a  11763  lediv12a  11798  elfzd  13176  fzass4  13223  4fvwrd4  13305  leexp1a  13821  wrd2ind  14364  cshwidxm1  14448  rtrclreclem4  14700  coprmproddvdslem  16295  reumodprminv  16433  prmgaplem6  16685  mreexexlem2d  17271  sgrp2nmndlem4  18482  pmtrrn2  18983  islmodd  20044  nn0srg  20580  rge0srg  20581  mdet1  21658  cpmatmcllem  21775  neitr  22239  restnlly  22541  llyrest  22544  llyidm  22547  uptx  22684  alexsubALTlem2  23107  alexsubALTlem4  23109  distspace  23377  ncvs1  24226  ivthlem3  24522  axtg5seg  26730  colperpexlem3  26997  outpasch  27020  iscgra1  27075  f1otrg  27136  ax5seg  27209  axcontlem4  27238  eengtrkg  27257  wlkonwlk1l  27933  crctcshwlkn0  28087  wwlksnextinj  28165  wwlksnextsurj  28166  clwwlkf1  28314  clwwlknon1  28362  numclwwlk1lem2f1  28622  wlkl0  28632  grpoidinv  28771  pjnmopi  30411  cdj1i  30696  xrofsup  30992  ccfldsrarelvec  31643  dya2iocnrect  32148  omssubadd  32167  sitgfval  32208  bnj969  32826  bnj1463  32935  erdszelem7  33059  rellysconn  33113  conway  33920  segconeq  34239  ifscgr  34273  btwnconn1lem13  34328  btwnconn1lem14  34329  outsideofeq  34359  ellines  34381  fnessref  34473  refssfne  34474  knoppndvlem14  34632  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  itg2gt0cn  35759  frinfm  35820  heiborlem3  35898  isfldidl  36153  4atlem12  37553  cdleme48fv  38440  cdlemg35  38654  mapd0  39606  leexp1ad  39907  aks4d1p1p5  40011  flt4lem7  40412  nna4b4nsq  40413  3cubeslem1  40422  mzpincl  40472  mzpindd  40484  diophin  40510  pellexlem3  40569  pellexlem5  40571  amgm3d  41699  amgm4d  41700  lptre2pt  43071  dvnprodlem2  43378  stoweidlem1  43432  stoweidlem14  43445  stoweidlem17  43448  stoweidlem27  43458  stoweidlem57  43488  fourierdlem12  43550  fourierdlem14  43552  fourierdlem70  43607  fourierdlem92  43629  fourierdlem111  43648  etransclem10  43675  etransclem24  43689  salgenval  43752  smfaddlem1  44185  f1cof1blem  44455  elfzelfzlble  44701  reuopreuprim  44866  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  lmod1  45721  inlinecirc02plem  46020