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  3862  domssl  8972  domssr  8973  sbthlem9  9065  nqerf  10890  lemul12a  12047  lediv12a  12083  elfzd  13483  fzass4  13530  4fvwrd4  13616  leexp1a  14147  wrd2ind  14695  cshwidxm1  14779  rtrclreclem4  15034  coprmproddvdslem  16639  reumodprminv  16782  prmgaplem6  17034  mreexexlem2d  17613  sgrp2nmndlem4  18862  pmtrrn2  19397  rngcinv  20553  ringcinv  20587  islmodd  20779  nn0srg  21361  rge0srg  21362  mdet1  22495  cpmatmcllem  22612  neitr  23074  restnlly  23376  llyrest  23379  llyidm  23382  uptx  23519  alexsubALTlem2  23942  alexsubALTlem4  23944  distspace  24211  ncvs1  25064  ivthlem3  25361  conway  27718  uzsind  28300  renegscl  28356  readdscl  28357  remulscl  28360  axtg5seg  28399  colperpexlem3  28666  outpasch  28689  iscgra1  28744  f1otrg  28805  ax5seg  28872  axcontlem4  28901  eengtrkg  28920  wlkonwlk1l  29598  crctcshwlkn0  29758  wwlksnextinj  29836  wwlksnextsurj  29837  clwwlkf1  29985  clwwlknon1  30033  numclwwlk1lem2f1  30293  wlkl0  30303  grpoidinv  30444  pjnmopi  32084  cdj1i  32369  xrofsup  32697  ccfldsrarelvec  33673  dya2iocnrect  34279  omssubadd  34298  sitgfval  34339  bnj969  34943  bnj1463  35052  erdszelem7  35191  rellysconn  35245  segconeq  36005  ifscgr  36039  btwnconn1lem13  36094  btwnconn1lem14  36095  outsideofeq  36125  ellines  36147  fnessref  36352  refssfne  36353  knoppndvlem14  36520  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlssretop  37358  itg2gt0cn  37676  frinfm  37736  heiborlem3  37814  isfldidl  38069  4atlem12  39613  cdleme48fv  40500  cdlemg35  40714  mapd0  41666  aks4d1p1p5  42070  flt4lem7  42654  nna4b4nsq  42655  3cubeslem1  42679  mzpincl  42729  mzpindd  42741  diophin  42767  pellexlem3  42826  pellexlem5  42828  dfno2  43424  amgm3d  44195  amgm4d  44196  lptre2pt  45645  dvnprodlem2  45952  stoweidlem1  46006  stoweidlem14  46019  stoweidlem17  46022  stoweidlem27  46032  stoweidlem57  46062  fourierdlem12  46124  fourierdlem14  46126  fourierdlem70  46181  fourierdlem92  46203  fourierdlem111  46222  etransclem10  46249  etransclem24  46263  salgenval  46326  smfaddlem1  46768  f1cof1blem  47079  elfzelfzlble  47326  reuopreuprim  47531  gpgedgvtx0  48056  rngcinvALTV  48268  ringcinvALTV  48302  lmod1  48485  inlinecirc02plem  48779  nelsubclem  49060  oppf1st2nd  49124