ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jca Structured version   GIF version

Theorem jca 290
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
StepHypRef Expression
1 jca.1 . 2 (φψ)
2 jca.2 . 2 (φχ)
3 pm3.2 126 . 2 (ψ → (χ → (ψ χ)))
41, 2, 3sylc 56 1 (φ → (ψ χ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  jca31  292  jca32  293  jcai  294  jctil  295  jctir  296  ancli  306  ancri  307  sylanbrc  394  jcab  535  ioran  668  ordi  728  dfandc  777  stabtestimpdc  823  pm4.55dc  845  mpbi2and  849  mpbir2and  850  pm4.82  856  pm4.83dc  857  rnlem  882  syl22anc  1135  syl112anc  1138  syl121anc  1139  syl211anc  1140  syl23anc  1141  syl32anc  1142  syl122anc  1143  syl212anc  1144  syl221anc  1145  syl222anc  1150  syl123anc  1151  syl132anc  1152  syl213anc  1153  syl231anc  1154  syl312anc  1155  syl321anc  1156  syl223anc  1160  syl232anc  1161  syl322anc  1162  syl233anc  1163  syl323anc  1164  syl332anc  1165  ecased  1238  19.26  1367  nfand  1457  19.40  1519  equsexd  1614  sbcof2  1688  sbequ8  1724  eu2  1941  eu3h  1942  eu5  1944  mooran2  1970  datisi  2007  felapton  2011  darapti  2012  dimatis  2014  fresison  2015  fesapo  2017  r19.26  2435  r19.29af2  2446  r19.40  2458  eqvinc  2661  eqvincg  2662  reu6  2724  reu3  2725  indifdir  3187  undif3ss  3192  un00  3257  disjpr2  3425  prel12  3533  prneimg  3536  preqsn  3537  opexgOLD  3956  opth  3965  0nelop  3976  euotd  3982  opelopabsb  3988  ispod  4032  elon2  4079  unexb  4143  opeluu  4148  eusvnfb  4152  suc11g  4235  nlimsucg  4242  tfi  4248  vtoclr  4331  opthprc  4334  ideqg  4430  resiexg  4596  dminss  4681  imainss  4682  ssxpbm  4699  relrelss  4787  funopg  4877  fntpg  4898  fun11uni  4912  imain  4924  funimaexglem  4925  funssxp  5003  ffdm  5004  f00  5024  dffo2  5053  fodmrnu  5057  foco  5059  fun11iun  5090  f1o00  5104  fv3  5140  dff2  5254  dff3im  5255  dffo4  5258  ffnfv  5266  ffvresb  5271  fsn2  5280  fconstfvm  5322  fnfvima  5336  fcof1o  5372  isocnv  5394  isotr  5399  riotaprop  5434  acexmidlemcase  5450  caovlem2d  5635  f1ocnvd  5644  caofcom  5676  resfunexgALT  5679  elxp7  5739  2ndrn  5751  1stconst  5784  2ndconst  5785  cnvf1olem  5787  poxp  5794  dftpos4  5819  dfsmo2  5843  tfrlem5  5871  tfrlemiex  5886  rdgon  5913  frecabex  5923  frecrdg  5931  oawordi  5988  nntri3  6014  nnmordi  6025  iserd  6068  relelec  6082  erth  6086  qliftfun  6124  bren  6164  elni2  6298  dfplpq2  6338  dfmpq2  6339  enqbreq2  6341  enqdc1  6346  addcmpblnq  6351  addclnq  6359  nqpi  6362  addassnqg  6366  mulassnqg  6368  mulcanenq  6369  distrnqg  6371  1qec  6372  recexnq  6374  subhalfnqq  6397  enq0tr  6416  nqnq0pi  6420  nq0nn  6424  mulcanenq0ec  6427  nnnq0lem1  6428  addclnq0  6433  distrnq0  6441  addassnq0lemcl  6443  elnp1st2nd  6458  prarloc  6485  addlocprlemlt  6514  addlocprlemeq  6516  addlocprlemgt  6517  addclpr  6520  nqprm  6525  mullocprlem  6549  mullocpr  6550  mulclpr  6551  ltpopr  6567  ltaddpr  6569  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemrnd  6577  ltexprlemdisj  6578  addcanprleml  6586  addcanprlemu  6587  addcanprg  6588  recexprlemm  6594  recexprlemopl  6595  recexprlemopu  6597  recexprlemrnd  6599  recexprlemdisj  6600  prsrlem1  6630  mulclsr  6642  mulasssrg  6646  distrsrg  6647  elreal2  6688  axmulass  6717  axdistr  6718  add20  7224  mullt0  7230  rereim  7330  ltmul1  7336  cru  7346  mulap0r  7359  divmuldivap  7430  divmuleqap  7435  divadddivap  7445  ltmul12a  7567  lemul12a  7569  lemulge11  7573  lediv12a  7601  lediv2a  7602  recgt1i  7605  recreclt  7607  ledivp1  7610  lemul1ad  7646  lemul2ad  7647  ltmul12ad  7648  lemul12ad  7649  lemul12bd  7650  nndivre  7690  nndivtr  7696  halfaddsubcl  7895  halfaddsub  7896  lt2halves  7897  nnrecl  7915  elnn0nn  7960  elnnnn0b  7962  elnnnn0c  7963  nn0addge1  7964  nn0addge2  7965  elnn0z  7994  elnnz1  8004  elz2  8048  zdivadd  8065  zdivmul  8066  zextle  8067  peano2uz2  8081  uzind  8085  btwnz  8093  uzss  8229  eluzp1m1  8232  eluz2b2  8276  qre  8296  qaddcl  8306  qmulcl  8308  qreccl  8311  irradd  8315  irrmul  8316  cnref1o  8317  rprege0  8332  rprene0  8335  rpreap0  8336  rpcnne0  8337  rpcnap0  8338  rpregt0d  8363  rprege0d  8364  rprene0d  8365  rpcnne0d  8366  lediv2ad  8379  lediv12ad  8412  xrlttri3  8448  xrrebnd  8462  xrrege0  8468  elioo4g  8533  ioomax  8547  iccmax  8548  divelunit  8600  elfz5  8612  uzsubsubfz  8641  fzopth  8654  fzass4  8655  fzrev2  8677  uzsplit  8684  elfz2nn0  8703  difelfzle  8722  1fv  8726  4fvwrd4  8727  fzo1fzo0n0  8769  elfzom1elp1fzo  8788  expclzaplem  8893  leexp1a  8923  expubnd  8925  le2sq2  8942  sumsqeq0  8945  bernneq  8982  expnlbnd  8986  bdop  9264  bdunexb  9305  bj-om  9325  findset  9333  bj-peano4  9343  bj-inf2vn  9358  bj-inf2vn2  9359
  Copyright terms: Public domain W3C validator