Theorem jca 300

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 137	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒)))
4	1, 2, 3	sylc 61	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  jca31  302  jca32  303  jcai  304  jctil  305  jctir  306  ancli  316  ancri  317  sylanbrc  408  jcab  567  ioran  701  ordi  762  dfandc  811  stabtestimpdc  857  pm4.55dc  879  mpbi2and  884  mpbir2and  885  pm4.82  891  pm4.83dc  892  rnlem  917  syl22anc  1170  syl112anc  1173  syl121anc  1174  syl211anc  1175  syl23anc  1176  syl32anc  1177  syl122anc  1178  syl212anc  1179  syl221anc  1180  syl222anc  1185  syl123anc  1186  syl132anc  1187  syl213anc  1188  syl231anc  1189  syl312anc  1190  syl321anc  1191  syl223anc  1195  syl232anc  1196  syl322anc  1197  syl233anc  1198  syl323anc  1199  syl332anc  1200  ecased  1280  19.26  1410  nfand  1500  19.40  1562  equsexd  1657  sbcof2  1731  sbequ8  1768  eu2  1985  eu3h  1986  eu5  1988  mooran2  2014  datisi  2051  felapton  2055  darapti  2056  dimatis  2058  fresison  2059  fesapo  2061  r19.26  2485  r19.29af2  2496  r19.40  2508  eqvinc  2718  eqvincg  2719  reu6  2781  reu3  2782  indifdir  3220  undif3ss  3225  un00  3290  disjpr2  3456  prel12  3563  prneimg  3566  preqsn  3567  opth  3992  0nelop  4003  euotd  4009  opelopabsb  4015  ispod  4059  elon2  4131  unexb  4195  opeluu  4200  eusvnfb  4204  suc11g  4300  nlimsucg  4309  tfi  4323  vtoclr  4406  opthprc  4409  ideqg  4505  resiexg  4673  dminss  4758  imainss  4759  ssxpbm  4776  relrelss  4864  funopg  4954  fntpg  4975  fun11uni  4989  imain  5001  funimaexglem  5002  funssxp  5080  ffdm  5081  f00  5101  dffo2  5130  fodmrnu  5134  foco  5136  fun11iun  5167  f1o00  5181  fv3  5218  dff2  5332  dff3im  5333  dffo4  5336  ffnfv  5344  ffvresb  5349  fsn2  5358  fconstfvm  5400  fnfvima  5414  fcof1o  5449  isocnv  5471  isotr  5476  riotaprop  5511  acexmidlemcase  5527  caovlem2d  5713  f1ocnvd  5722  caofcom  5754  resfunexgALT  5757  elxp7  5817  2ndrn  5829  1stconst  5862  2ndconst  5863  cnvf1olem  5865  poxp  5873  dftpos4  5901  dfsmo2  5925  tfrlem5  5953  tfrlemiex  5968  rdgon  5996  frecabex  6007  frecrdg  6015  oawordi  6072  nntri3  6098  nnmordi  6112  iserd  6155  relelec  6169  erth  6173  qliftfun  6211  bren  6251  findcard2d  6375  findcard2sd  6376  nnwetri  6382  supisolem  6421  ordiso2  6446  elni2  6504  dfplpq2  6544  dfmpq2  6545  enqbreq2  6547  enqdc1  6552  addcmpblnq  6557  addclnq  6565  nqpi  6568  addassnqg  6572  mulassnqg  6574  mulcanenq  6575  distrnqg  6577  1qec  6578  recexnq  6580  subhalfnqq  6604  enq0tr  6624  nqnq0pi  6628  nq0nn  6632  mulcanenq0ec  6635  nnnq0lem1  6636  addclnq0  6641  distrnq0  6649  addassnq0lemcl  6651  elnp1st2nd  6666  prarloc  6693  addlocprlemlt  6721  addlocprlemeq  6723  addlocprlemgt  6724  addclpr  6727  nqprm  6732  mullocprlem  6760  mullocpr  6761  mulclpr  6762  ltpopr  6785  ltaddpr  6787  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemrnd  6795  ltexprlemdisj  6796  addcanprleml  6804  addcanprlemu  6805  addcanprg  6806  recexprlemm  6814  recexprlemopl  6815  recexprlemopu  6817  recexprlemrnd  6819  recexprlemdisj  6820  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemopu  6838  cauappcvgprlemrnd  6840  cauappcvgprlemdisj  6841  cauappcvgprlemlim  6851  caucvgprlemnkj  6856  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemopu  6861  caucvgprlemrnd  6863  caucvgprlemlim  6871  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemm  6886  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemrnd  6891  caucvgprprlemexbt  6896  caucvgprprlemlim  6901  prsrlem1  6919  mulclsr  6931  mulasssrg  6935  distrsrg  6936  elreal2  6999  axmulass  7039  axdistr  7040  axcaucvglemcau  7064  add20  7578  mullt0  7584  rereim  7686  ltmul1  7692  cru  7702  mulap0r  7715  divmuldivap  7800  divmuleqap  7805  divadddivap  7815  divmuldivapd  7918  ltmul12a  7938  lemul12a  7940  lemulge11  7944  lediv12a  7972  lediv2a  7973  recgt1i  7976  recreclt  7978  ledivp1  7981  lemul1ad  8017  lemul2ad  8018  ltmul12ad  8019  lemul12ad  8020  lemul12bd  8021  nndivre  8074  nndivtr  8080  halfaddsubcl  8264  halfaddsub  8265  lt2halves  8266  nnrecl  8286  elnn0nn  8330  elnnnn0b  8332  elnnnn0c  8333  nn0addge1  8334  nn0addge2  8335  elnn0z  8364  elnnz1  8374  nzadd  8403  elz2  8419  zdivadd  8436  zdivmul  8437  zextle  8438  peano2uz2  8454  uzind  8458  btwnz  8466  uzss  8639  eluzp1m1  8642  eluz2b2  8690  qre  8710  qaddcl  8720  qmulcl  8722  qreccl  8727  irradd  8731  irrmul  8732  cnref1o  8733  rprege0  8748  rprene0  8751  rpreap0  8752  rpcnne0  8753  rpcnap0  8754  rpregt0d  8780  rprege0d  8781  rprene0d  8782  rpcnne0d  8783  lediv2ad  8796  ledivge1le  8803  lediv12ad  8833  nnledivrp  8837  nn0ledivnn  8838  xrlttri3  8872  xrrebnd  8886  xrrege0  8892  elioo4g  8957  ioomax  8971  iccmax  8972  divelunit  9024  elfz5  9037  uzsubsubfz  9066  fzopth  9079  fzass4  9080  fzrev2  9102  uzsplit  9109  elfz2nn0  9128  difelfzle  9145  1fv  9149  4fvwrd4  9150  fzo1fzo0n0  9192  elfzom1elp1fzo  9211  subfzo0  9251  qtri3or  9252  adddivflid  9294  flltdivnn0lt  9306  intfracq  9322  modqid2  9353  modfzo0difsn  9397  expclzaplem  9500  leexp1a  9531  expubnd  9533  le2sq2  9551  sumsqeq0  9554  bernneq  9593  expnlbnd  9597  nn0opthd  9649  faclbnd6  9671  facavg  9673  shftlem  9704  shftfvalg  9706  shftfval  9709  cvg1nlemcau  9870  cvg1nlemres  9871  rexuz3  9876  resqrexlemcvg  9905  resqrexlemglsq  9908  resqrexlemga  9909  sqrtle  9922  sqrtlt  9923  sqrt11  9925  sqrtsq2  9929  absmul  9955  sqabs  9968  abslt  9974  absle  9975  lenegsq  9981  maxleastb  10100  maxltsup  10104  rexanre  10106  negfi  10110  climcn2  10148  mulcn2  10151  dvdsval3  10199  dvdscmul  10222  dvdsmulc  10223  dvdscmulr  10224  dvdsmulcr  10225  modmulconst  10227  dvds2ln  10228  ltoddhalfle  10293  nn0o  10307  divalg2  10326  ndvdssub  10330  ndvdsadd  10331  infssuzex  10345  divgcdz  10363  gcd0id  10370  gcdaddm  10375  bezoutlemstep  10386  bezoutlemmain  10387  dfgcd3  10399  dfgcd2  10403  lcmcllem  10449  dvdslcm  10451  lcmgcdlem  10459  lcmgcdnn  10464  qredeq  10478  qredeu  10479  rpdvds  10481  divgcdcoprm0  10483  cncongr1  10485  cncongr2  10486  cncongrcoprm  10488  prmind2  10502  isprm6  10526  prmexpb  10530  cncongrprm  10536  sqrt2irrlem  10540  pw2dvdslemn  10543  oddpwdclemxy  10547  oddpwdclemdc  10551  oddpwdc  10552  bdop  10666  bdunexb  10711  bj-om  10732  findset  10740  bj-peano4  10750  bj-inf2vn  10769  bj-inf2vn2  10770  qdencn  10785