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  3850  domssl  8930  domssr  8931  sbthlem9  9019  nqerf  10843  lemul12a  12000  lediv12a  12036  elfzd  13436  fzass4  13483  4fvwrd4  13569  leexp1a  14100  wrd2ind  14647  cshwidxm1  14731  rtrclreclem4  14986  coprmproddvdslem  16591  reumodprminv  16734  prmgaplem6  16986  mreexexlem2d  17569  sgrp2nmndlem4  18820  pmtrrn2  19357  rngcinv  20540  ringcinv  20574  islmodd  20787  nn0srg  21362  rge0srg  21363  mdet1  22504  cpmatmcllem  22621  neitr  23083  restnlly  23385  llyrest  23388  llyidm  23391  uptx  23528  alexsubALTlem2  23951  alexsubALTlem4  23953  distspace  24220  ncvs1  25073  ivthlem3  25370  conway  27728  uzsind  28316  renegscl  28385  readdscl  28386  remulscl  28389  axtg5seg  28428  colperpexlem3  28695  outpasch  28718  iscgra1  28773  f1otrg  28834  ax5seg  28901  axcontlem4  28930  eengtrkg  28949  wlkonwlk1l  29625  crctcshwlkn0  29784  wwlksnextinj  29862  wwlksnextsurj  29863  clwwlkf1  30011  clwwlknon1  30059  numclwwlk1lem2f1  30319  wlkl0  30329  grpoidinv  30470  pjnmopi  32110  cdj1i  32395  xrofsup  32723  ccfldsrarelvec  33645  dya2iocnrect  34251  omssubadd  34270  sitgfval  34311  bnj969  34915  bnj1463  35024  erdszelem7  35172  rellysconn  35226  segconeq  35986  ifscgr  36020  btwnconn1lem13  36075  btwnconn1lem14  36076  outsideofeq  36106  ellines  36128  fnessref  36333  refssfne  36334  knoppndvlem14  36501  isbasisrelowllem1  37331  isbasisrelowllem2  37332  relowlssretop  37339  itg2gt0cn  37657  frinfm  37717  heiborlem3  37795  isfldidl  38050  4atlem12  39594  cdleme48fv  40481  cdlemg35  40695  mapd0  41647  aks4d1p1p5  42051  flt4lem7  42635  nna4b4nsq  42636  3cubeslem1  42660  mzpincl  42710  mzpindd  42722  diophin  42748  pellexlem3  42807  pellexlem5  42809  dfno2  43404  amgm3d  44175  amgm4d  44176  lptre2pt  45625  dvnprodlem2  45932  stoweidlem1  45986  stoweidlem14  45999  stoweidlem17  46002  stoweidlem27  46012  stoweidlem57  46042  fourierdlem12  46104  fourierdlem14  46106  fourierdlem70  46161  fourierdlem92  46183  fourierdlem111  46202  etransclem10  46229  etransclem24  46243  salgenval  46306  smfaddlem1  46748  f1cof1blem  47062  elfzelfzlble  47309  reuopreuprim  47514  gpgedgvtx0  48049  rngcinvALTV  48264  ringcinvALTV  48298  lmod1  48481  inlinecirc02plem  48775  nelsubclem  49056  oppf1st2nd  49120