Theorem jca 302

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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  jca31  305  jca32  306  jcai  307  jctil  308  jctir  309  ancli  319  ancri  320  sylanbrc  411  jcab  575  ioran  724  ordi  788  stdcndc  813  stdcndcOLD  814  dfandc  852  pm4.55dc  905  mpbi2and  910  mpbir2and  911  pm4.82  917  pm4.83dc  918  rnlem  943  syl22anc  1200  syl112anc  1203  syl121anc  1204  syl211anc  1205  syl23anc  1206  syl32anc  1207  syl122anc  1208  syl212anc  1209  syl221anc  1210  syl222anc  1215  syl123anc  1216  syl132anc  1217  syl213anc  1218  syl231anc  1219  syl312anc  1220  syl321anc  1221  syl223anc  1225  syl232anc  1226  syl322anc  1227  syl233anc  1228  syl323anc  1229  syl332anc  1230  ecased  1310  19.26  1440  nfand  1530  19.40  1593  equsexd  1690  sbcof2  1764  sbequ8  1801  eu2  2019  eu3h  2020  eu5  2022  mooran2  2048  datisi  2085  felapton  2089  darapti  2090  dimatis  2092  fresison  2093  fesapo  2095  reximssdv  2510  r19.26  2532  r19.29af2  2546  r19.40  2559  eqvinc  2778  eqvincg  2779  elrabd  2811  reu6  2842  reu3  2843  indifdir  3298  undif3ss  3303  un00  3375  eqifdc  3472  disjpr2  3553  prel12  3664  prneimg  3667  preqsn  3668  disjiun  3890  opth  4119  0nelop  4130  euotd  4136  opelopabsb  4142  ispod  4186  elon2  4258  unexb  4323  opeluu  4331  eusvnfb  4335  suc11g  4432  nlimsucg  4441  tfi  4456  vtoclr  4547  opthprc  4550  ideqg  4650  resiexg  4822  dminss  4911  imainss  4912  ssxpbm  4932  relrelss  5023  funopg  5115  fntpg  5137  fun11uni  5151  imain  5163  funimaexglem  5164  funssxp  5250  ffdm  5251  f00  5272  dffo2  5307  fodmrnu  5311  foco  5313  fun11iun  5344  f1o00  5358  fv3  5398  dff2  5518  dff3im  5519  dffo4  5522  ffnfv  5532  ffvresb  5537  fsn2  5548  fconstfvm  5592  fnfvima  5606  fcof1o  5644  isocnv  5666  isotr  5671  riotaprop  5707  acexmidlemcase  5723  caovlem2d  5917  f1ocnvd  5926  caofcom  5959  resfunexgALT  5962  elxp7  6022  2ndrn  6035  1stconst  6072  2ndconst  6073  cnvf1olem  6075  poxp  6083  dftpos4  6114  dfsmo2  6138  tfrlem5  6165  tfrlemiex  6182  tfr1onlemsucaccv  6192  tfr1onlembfn  6195  tfr1onlemex  6198  tfr1onlemres  6200  tfrcllemsucaccv  6205  tfrcllembfn  6208  tfrcllemex  6211  tfrcllemres  6213  tfrcl  6215  frecabex  6249  frecabcl  6250  frecfcllem  6255  frecrdg  6259  oawordi  6319  nntri3  6347  nntr2  6353  nnmordi  6366  iserd  6409  relelec  6423  erth  6427  qliftfun  6465  mapsncnv  6543  mptelixpg  6582  bren  6595  findcard2d  6738  findcard2sd  6739  isinfinf  6744  tridc  6746  nnwetri  6757  undifdcss  6764  fiintim  6770  fisseneq  6773  fidcenumlemim  6792  sbthlemi9  6805  supisolem  6847  ordiso2  6872  updjud  6919  difinfsn  6937  ctssdccl  6948  acfun  7011  elni2  7067  dfplpq2  7107  dfmpq2  7108  enqbreq2  7110  enqdc1  7115  addcmpblnq  7120  addclnq  7128  nqpi  7131  addassnqg  7135  mulassnqg  7137  mulcanenq  7138  distrnqg  7140  1qec  7141  recexnq  7143  subhalfnqq  7167  enq0tr  7187  nqnq0pi  7191  nq0nn  7195  mulcanenq0ec  7198  nnnq0lem1  7199  addclnq0  7204  distrnq0  7212  addassnq0lemcl  7214  elnp1st2nd  7229  prarloc  7256  addlocprlemlt  7284  addlocprlemeq  7286  addlocprlemgt  7287  addclpr  7290  nqprm  7295  mullocprlem  7323  mullocpr  7324  mulclpr  7325  ltpopr  7348  ltaddpr  7350  ltexprlemm  7353  ltexprlemopl  7354  ltexprlemopu  7356  ltexprlemrnd  7358  ltexprlemdisj  7359  addcanprleml  7367  addcanprlemu  7368  addcanprg  7369  recexprlemm  7377  recexprlemopl  7378  recexprlemopu  7380  recexprlemrnd  7382  recexprlemdisj  7383  cauappcvgprlemm  7398  cauappcvgprlemopl  7399  cauappcvgprlemopu  7401  cauappcvgprlemrnd  7403  cauappcvgprlemdisj  7404  cauappcvgprlemlim  7414  caucvgprlemnkj  7419  caucvgprlemm  7421  caucvgprlemopl  7422  caucvgprlemopu  7424  caucvgprlemrnd  7426  caucvgprlemlim  7434  caucvgprprlemnkltj  7442  caucvgprprlemnkeqj  7443  caucvgprprlemnjltk  7444  caucvgprprlemm  7449  caucvgprprlemopl  7450  caucvgprprlemopu  7452  caucvgprprlemrnd  7454  caucvgprprlemexbt  7459  caucvgprprlemlim  7464  prsrlem1  7482  mulclsr  7494  mulasssrg  7498  distrsrg  7499  elreal2  7562  axmulass  7605  axdistr  7606  axcaucvglemcau  7630  add20  8152  mullt0  8158  rereim  8263  ltmul1  8269  cru  8279  mulap0r  8292  divmuldivap  8382  divmuleqap  8387  divadddivap  8397  divmuldivapd  8502  div2subap  8506  ltmul12a  8525  lemul12a  8527  lemulge11  8531  lediv12a  8559  lediv2a  8560  recgt1i  8563  recreclt  8565  ledivp1  8568  lemul1ad  8604  lemul2ad  8605  ltmul12ad  8606  lemul12ad  8607  lemul12bd  8608  nndivre  8663  nndivtr  8669  halfaddsubcl  8854  halfaddsub  8855  lt2halves  8856  nnrecl  8876  elnn0nn  8920  elnnnn0b  8922  elnnnn0c  8923  nn0addge1  8924  nn0addge2  8925  xnn0xrnemnf  8953  elnn0z  8968  elnnz1  8978  nzadd  9007  elz2  9023  zdivadd  9041  zdivmul  9042  zextle  9043  peano2uz2  9059  uzind  9063  btwnz  9071  uzss  9245  eluzp1m1  9248  eluz2b2  9296  qre  9316  qaddcl  9326  qmulcl  9328  qreccl  9333  irradd  9337  irrmul  9338  cnref1o  9339  rprege0  9354  rprene0  9357  rpreap0  9358  rpcnne0  9359  rpcnap0  9360  rpregt0d  9386  rprege0d  9387  rprene0d  9388  rpcnne0d  9389  lediv2ad  9402  ledivge1le  9409  lediv12ad  9439  nnledivrp  9443  nn0ledivnn  9444  xrlttri3  9473  xrrebnd  9492  xrrege0  9498  xnn0xadd0  9540  xlesubadd  9556  elioo4g  9607  ioomax  9621  iccmax  9622  divelunit  9675  elfz5  9688  uzsubsubfz  9717  fzopth  9731  fzass4  9732  fzrev2  9755  uzsplit  9762  elfz2nn0  9782  difelfzle  9801  1fv  9806  4fvwrd4  9807  fzo1fzo0n0  9850  elfzom1elp1fzo  9869  subfzo0  9909  qtri3or  9910  adddivflid  9955  flltdivnn0lt  9967  intfracq  9983  modqid2  10014  modfzo0difsn  10058  seq3val  10121  seqvalcd  10122  iseqf1olemqcl  10149  iseqf1olemnab  10151  iseqf1olemab  10152  iseqf1olemmo  10155  seq3f1olemqsumkj  10161  seq3f1olemqsumk  10162  expclzaplem  10207  leexp1a  10238  expubnd  10240  le2sq2  10258  sumsqeq0  10261  bernneq  10302  expnlbnd  10306  nn0opthd  10358  faclbnd6  10380  facavg  10382  seq3coll  10475  shftlem  10478  shftfvalg  10480  shftfval  10483  cvg1nlemcau  10645  cvg1nlemres  10646  rexuz3  10651  resqrexlemcvg  10680  resqrexlemglsq  10683  resqrexlemga  10684  sqrtle  10697  sqrtlt  10698  sqrt11  10700  sqrtsq2  10704  absmul  10730  sqabs  10743  abslt  10749  absle  10750  lenegsq  10756  maxleastb  10875  maxltsup  10879  rexanre  10881  negfi  10888  xrmaxiflemab  10905  xrmaxiflemlub  10906  xrmaxltsup  10916  xrmaxadd  10919  climcn2  10967  mulcn2  10970  summodclem2a  11039  summodc  11041  fsum3  11045  fsum3cvg3  11054  fsumcl2lem  11056  fsumadd  11064  fsump1i  11091  fsum0diaglem  11098  mptfzshft  11100  fsumrev  11101  fsummulc2  11106  fsum00  11120  expcnvap0  11160  mertenslemi1  11193  eftlub  11244  efieq  11290  sincos1sgn  11319  demoivreALT  11327  dvdsval3  11342  dvdscmul  11365  dvdsmulc  11366  dvdscmulr  11367  dvdsmulcr  11368  modmulconst  11370  dvds2ln  11371  ltoddhalfle  11435  nn0o  11449  divalg2  11468  ndvdssub  11472  ndvdsadd  11473  infssuzex  11487  divgcdz  11505  gcd0id  11512  gcdaddm  11517  bezoutlemstep  11528  bezoutlemmain  11529  dfgcd3  11541  dfgcd2  11545  lcmcllem  11591  dvdslcm  11593  lcmgcdlem  11601  lcmgcdnn  11606  qredeq  11620  qredeu  11621  rpdvds  11623  divgcdcoprm0  11625  cncongr1  11627  cncongr2  11628  cncongrcoprm  11630  prmind2  11644  isprm6  11668  prmexpb  11672  cncongrprm  11678  sqrt2irrlem  11682  pw2dvdslemn  11685  oddpwdclemxy  11689  oddpwdclemdc  11693  oddpwdc  11694  hashdvds  11739  hashgcdlem  11745  ennnfonelemfun  11772  ennnfonelemim  11779  ctinfomlemom  11782  ctinfom  11783  ctinf  11785  ctiunctlemfo  11792  topgele  12036  tgcl  12073  epttop  12099  opnssneib  12165  iscnp4  12226  cnco  12229  cncnp  12238  cnrest2  12244  lmss  12254  txcnp  12279  txcn  12283  cnmpt12  12295  cnmpt22  12302  psmetres2  12319  distspace  12321  ismeti  12332  isxmetd  12333  xmetpsmet  12355  xblss2ps  12390  xblss2  12391  blcntrps  12401  blcntr  12402  blin2  12418  mopni3  12470  metequiv2  12482  bdmet  12488  xmettx  12496  cnbl0  12520  cnblcld  12521  tgioo  12529  elcncf1di  12549  cnplimcim  12589  limccnp2lem  12598  dvfvalap  12602  bj-nnan  12635  bdop  12757  bdunexb  12802  bj-om  12819  findset  12827  bj-peano4  12837  bj-inf2vn  12856  bj-inf2vn2  12857  pwle2  12877  pwf1oexmid  12878  nninfalllemn  12886  sbthom  12905  qdencn  12906  trilpolemlt1  12918