Theorem jca 304

Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
jca.1	⊢ (𝜑 → 𝜓)
jca.2	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
jca	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. 2 ⊢ (𝜑 → 𝜓)
2		jca.2	. 2 ⊢ (𝜑 → 𝜒)
3		pm3.2 138	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒)))
4	1, 2, 3	sylc 62	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jca31  307  jca32  308  jcai  309  jctil  310  jctir  311  ancli  321  ancri  322  sylanbrc  413  jcab  592  ioran  741  ordi  805  stdcndc  830  stdcndcOLD  831  dfandc  869  pm4.55dc  922  mpbi2and  927  mpbir2and  928  pm4.82  934  pm4.83dc  935  rnlem  960  syl22anc  1217  syl112anc  1220  syl121anc  1221  syl211anc  1222  syl23anc  1223  syl32anc  1224  syl122anc  1225  syl212anc  1226  syl221anc  1227  syl222anc  1232  syl123anc  1233  syl132anc  1234  syl213anc  1235  syl231anc  1236  syl312anc  1237  syl321anc  1238  syl223anc  1242  syl232anc  1243  syl322anc  1244  syl233anc  1245  syl323anc  1246  syl332anc  1247  ecased  1327  19.26  1457  nfand  1547  19.40  1610  equsexd  1707  sbcof2  1782  sbequ8  1819  eu2  2041  eu3h  2042  eu5  2044  mooran2  2070  datisi  2107  felapton  2111  darapti  2112  dimatis  2114  fresison  2115  fesapo  2117  reximssdv  2534  r19.26  2556  r19.29af2  2570  r19.40  2583  eqvinc  2803  eqvincg  2804  elrabd  2837  reu6  2868  reu3  2869  indifdir  3327  undif3ss  3332  un00  3404  eqifdc  3501  disjpr2  3582  prel12  3693  prneimg  3696  preqsn  3697  disjiun  3919  opth  4154  0nelop  4165  euotd  4171  opelopabsb  4177  ispod  4221  elon2  4293  unexb  4358  opeluu  4366  eusvnfb  4370  suc11g  4467  nlimsucg  4476  tfi  4491  vtoclr  4582  opthprc  4585  ideqg  4685  resiexg  4859  dminss  4948  imainss  4949  ssxpbm  4969  relrelss  5060  funopg  5152  fntpg  5174  fun11uni  5188  imain  5200  funimaexglem  5201  funssxp  5287  ffdm  5288  f00  5309  dffo2  5344  fodmrnu  5348  foco  5350  fun11iun  5381  f1o00  5395  fsnd  5403  fv3  5437  dff2  5557  dff3im  5558  dffo4  5561  ffnfv  5571  ffvresb  5576  fsn2  5587  fconstfvm  5631  fnfvima  5645  fcof1o  5683  isocnv  5705  isotr  5710  riotaprop  5746  acexmidlemcase  5762  caovlem2d  5956  f1ocnvd  5965  caofcom  5998  resfunexgALT  6001  elxp7  6061  2ndrn  6074  1stconst  6111  2ndconst  6112  cnvf1olem  6114  poxp  6122  dftpos4  6153  dfsmo2  6177  tfrlem5  6204  tfrlemiex  6221  tfr1onlemsucaccv  6231  tfr1onlembfn  6234  tfr1onlemex  6237  tfr1onlemres  6239  tfrcllemsucaccv  6244  tfrcllembfn  6247  tfrcllemex  6250  tfrcllemres  6252  tfrcl  6254  frecabex  6288  frecabcl  6289  frecfcllem  6294  frecrdg  6298  oawordi  6358  nntri3  6386  nntr2  6392  nnmordi  6405  iserd  6448  relelec  6462  erth  6466  qliftfun  6504  mapsncnv  6582  mptelixpg  6621  bren  6634  findcard2d  6778  findcard2sd  6779  isinfinf  6784  tridc  6786  nnwetri  6797  undifdcss  6804  fiintim  6810  fisseneq  6813  fidcenumlemim  6833  sbthlemi9  6846  supisolem  6888  ordiso2  6913  updjud  6960  difinfsn  6978  ctssdccl  6989  acfun  7056  ccfunen  7072  elni2  7115  dfplpq2  7155  dfmpq2  7156  enqbreq2  7158  enqdc1  7163  addcmpblnq  7168  addclnq  7176  nqpi  7179  addassnqg  7183  mulassnqg  7185  mulcanenq  7186  distrnqg  7188  1qec  7189  recexnq  7191  subhalfnqq  7215  enq0tr  7235  nqnq0pi  7239  nq0nn  7243  mulcanenq0ec  7246  nnnq0lem1  7247  addclnq0  7252  distrnq0  7260  addassnq0lemcl  7262  elnp1st2nd  7277  prarloc  7304  addlocprlemlt  7332  addlocprlemeq  7334  addlocprlemgt  7335  addclpr  7338  nqprm  7343  mullocprlem  7371  mullocpr  7372  mulclpr  7373  ltpopr  7396  ltaddpr  7398  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemrnd  7406  ltexprlemdisj  7407  addcanprleml  7415  addcanprlemu  7416  addcanprg  7417  recexprlemm  7425  recexprlemopl  7426  recexprlemopu  7428  recexprlemrnd  7430  recexprlemdisj  7431  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemopu  7449  cauappcvgprlemrnd  7451  cauappcvgprlemdisj  7452  cauappcvgprlemlim  7462  caucvgprlemnkj  7467  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemopu  7472  caucvgprlemrnd  7474  caucvgprlemlim  7482  caucvgprprlemnkltj  7490  caucvgprprlemnkeqj  7491  caucvgprprlemnjltk  7492  caucvgprprlemm  7497  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemrnd  7502  caucvgprprlemexbt  7507  caucvgprprlemlim  7512  suplocexprlemrl  7518  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemex  7523  suplocexprlemub  7524  prsrlem1  7543  mulclsr  7555  mulasssrg  7559  distrsrg  7560  suplocsrlemb  7607  elreal2  7631  axmulass  7674  axdistr  7675  axcaucvglemcau  7699  add20  8229  mullt0  8235  rereim  8341  ltmul1  8347  cru  8357  mulap0r  8370  aprcl  8401  divmuldivap  8465  divmuleqap  8470  divadddivap  8480  divmuldivapd  8585  div2subap  8589  ltmul12a  8611  lemul12a  8613  lemulge11  8617  lediv12a  8645  lediv2a  8646  recgt1i  8649  recreclt  8651  ledivp1  8654  lemul1ad  8690  lemul2ad  8691  ltmul12ad  8692  lemul12ad  8693  lemul12bd  8694  nndivre  8749  nndivtr  8755  halfaddsubcl  8946  halfaddsub  8947  lt2halves  8948  nnrecl  8968  elnn0nn  9012  elnnnn0b  9014  elnnnn0c  9015  nn0addge1  9016  nn0addge2  9017  xnn0xrnemnf  9045  elnn0z  9060  elnnz1  9070  nzadd  9099  elz2  9115  zdivadd  9133  zdivmul  9134  zextle  9135  peano2uz2  9151  uzind  9155  btwnz  9163  uzss  9339  eluzp1m1  9342  eluz2b2  9390  qre  9410  qaddcl  9420  qmulcl  9422  qreccl  9427  irradd  9431  irrmul  9432  cnref1o  9433  rprege0  9449  rprene0  9452  rpreap0  9453  rpcnne0  9454  rpcnap0  9455  rpregt0d  9483  rprege0d  9484  rprene0d  9485  rpcnne0d  9486  lediv2ad  9499  ledivge1le  9506  lediv12ad  9536  nnledivrp  9546  nn0ledivnn  9547  xrlttri3  9576  xrrebnd  9595  xrrege0  9601  xnn0xadd0  9643  xlesubadd  9659  elioo4g  9710  ioomax  9724  iccmax  9725  divelunit  9778  elfz5  9791  uzsubsubfz  9820  fzopth  9834  fzass4  9835  fzrev2  9858  uzsplit  9865  elfz2nn0  9885  difelfzle  9904  1fv  9909  4fvwrd4  9910  fzo1fzo0n0  9953  elfzom1elp1fzo  9972  subfzo0  10012  qtri3or  10013  adddivflid  10058  flltdivnn0lt  10070  intfracq  10086  modqid2  10117  modfzo0difsn  10161  seq3val  10224  seqvalcd  10225  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  iseqf1olemmo  10258  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  expclzaplem  10310  leexp1a  10341  expubnd  10343  le2sq2  10361  sumsqeq0  10364  bernneq  10405  expnlbnd  10409  nn0opthd  10461  faclbnd6  10483  facavg  10485  seq3coll  10578  shftlem  10581  shftfvalg  10583  shftfval  10586  cvg1nlemcau  10749  cvg1nlemres  10750  rexuz3  10755  resqrexlemcvg  10784  resqrexlemglsq  10787  resqrexlemga  10788  sqrtle  10801  sqrtlt  10802  sqrt11  10804  sqrtsq2  10808  absmul  10834  sqabs  10847  abslt  10853  absle  10854  lenegsq  10860  maxleastb  10979  maxltsup  10983  rexanre  10985  negfi  10992  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxltsup  11020  xrmaxadd  11023  climcn2  11071  mulcn2  11074  summodclem2a  11143  summodc  11145  fsum3  11149  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  fsump1i  11195  fsum0diaglem  11202  mptfzshft  11204  fsumrev  11205  fsummulc2  11210  fsum00  11224  expcnvap0  11264  mertenslemi1  11297  ntrivcvgap0  11311  eftlub  11385  efieq  11431  sincos1sgn  11460  demoivreALT  11469  dvdsval3  11486  dvdscmul  11509  dvdsmulc  11510  dvdscmulr  11511  dvdsmulcr  11512  modmulconst  11514  dvds2ln  11515  ltoddhalfle  11579  nn0o  11593  divalg2  11612  ndvdssub  11616  ndvdsadd  11617  infssuzex  11631  divgcdz  11649  gcd0id  11656  gcdaddm  11661  bezoutlemstep  11674  bezoutlemmain  11675  dfgcd3  11687  dfgcd2  11691  lcmcllem  11737  dvdslcm  11739  lcmgcdlem  11747  lcmgcdnn  11752  qredeq  11766  qredeu  11767  rpdvds  11769  divgcdcoprm0  11771  cncongr1  11773  cncongr2  11774  cncongrcoprm  11776  prmind2  11790  isprm6  11814  prmexpb  11818  cncongrprm  11824  sqrt2irrlem  11828  pw2dvdslemn  11832  oddpwdclemxy  11836  oddpwdclemdc  11840  oddpwdc  11841  hashdvds  11886  hashgcdlem  11892  ennnfonelemfun  11919  ennnfonelemim  11926  ctinfomlemom  11929  ctinfom  11930  ctinf  11932  ctiunctlemfo  11941  topgele  12185  tgcl  12222  epttop  12248  opnssneib  12314  iscnp4  12376  cnco  12379  cncnp  12388  cnrest2  12394  lmss  12404  txcnp  12429  txcn  12433  cnmpt12  12445  cnmpt22  12452  hmeof1o  12467  psmetres2  12491  distspace  12493  ismeti  12504  isxmetd  12505  xmetpsmet  12527  xblss2ps  12562  xblss2  12563  blcntrps  12573  blcntr  12574  blin2  12590  mopni3  12642  metequiv2  12654  bdmet  12660  xmettx  12668  cnbl0  12692  cnblcld  12693  tgioo  12704  elcncf1di  12724  dedekindeulemlu  12757  suplociccex  12761  dedekindicclemlu  12766  dedekindicc  12769  ivthinclemlopn  12772  ivthdec  12780  cnplimcim  12794  limccnp2lem  12803  dvfvalap  12808  sin0pilem1  12851  pilem3  12853  ptolemy  12894  sincosq1sgn  12896  sinq12gt0  12900  bj-nnan  12937  bdop  13062  bdunexb  13107  bj-om  13124  findset  13132  bj-peano4  13142  bj-inf2vn  13161  bj-inf2vn2  13162  pwle2  13182  pwf1oexmid  13183  nninfalllemn  13191  sbthom  13210  qdencn  13211  trilpolemlt1  13223