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  6513  addlocprlemeq  6515  addlocprlemgt  6516  addclpr  6519  nqprm  6524  mullocprlem  6550  mullocpr  6551  mulclpr  6552  ltpopr  6568  ltaddpr  6570  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemrnd  6578  ltexprlemdisj  6579  addcanprleml  6587  addcanprlemu  6588  addcanprg  6589  recexprlemm  6595  recexprlemopl  6596  recexprlemopu  6598  recexprlemrnd  6600  recexprlemdisj  6601  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemopu  6619  cauappcvgprlemrnd  6621  cauappcvgprlemdisj  6622  cauappcvgprlemlim  6632  prsrlem1  6650  mulclsr  6662  mulasssrg  6666  distrsrg  6667  elreal2  6708  axmulass  6737  axdistr  6738  add20  7244  mullt0  7250  rereim  7350  ltmul1  7356  cru  7366  mulap0r  7379  divmuldivap  7450  divmuleqap  7455  divadddivap  7465  ltmul12a  7587  lemul12a  7589  lemulge11  7593  lediv12a  7621  lediv2a  7622  recgt1i  7625  recreclt  7627  ledivp1  7630  lemul1ad  7666  lemul2ad  7667  ltmul12ad  7668  lemul12ad  7669  lemul12bd  7670  nndivre  7710  nndivtr  7716  halfaddsubcl  7915  halfaddsub  7916  lt2halves  7917  nnrecl  7935  elnn0nn  7980  elnnnn0b  7982  elnnnn0c  7983  nn0addge1  7984  nn0addge2  7985  elnn0z  8014  elnnz1  8024  elz2  8068  zdivadd  8085  zdivmul  8086  zextle  8087  peano2uz2  8101  uzind  8105  btwnz  8113  uzss  8249  eluzp1m1  8252  eluz2b2  8296  qre  8316  qaddcl  8326  qmulcl  8328  qreccl  8331  irradd  8335  irrmul  8336  cnref1o  8337  rprege0  8352  rprene0  8355  rpreap0  8356  rpcnne0  8357  rpcnap0  8358  rpregt0d  8383  rprege0d  8384  rprene0d  8385  rpcnne0d  8386  lediv2ad  8399  lediv12ad  8432  xrlttri3  8468  xrrebnd  8482  xrrege0  8488  elioo4g  8553  ioomax  8567  iccmax  8568  divelunit  8620  elfz5  8632  uzsubsubfz  8661  fzopth  8674  fzass4  8675  fzrev2  8697  uzsplit  8704  elfz2nn0  8723  difelfzle  8742  1fv  8746  4fvwrd4  8747  fzo1fzo0n0  8789  elfzom1elp1fzo  8808  expclzaplem  8913  leexp1a  8943  expubnd  8945  le2sq2  8962  sumsqeq0  8965  bernneq  9002  expnlbnd  9006  bdop  9310  bdunexb  9351  bj-om  9371  findset  9379  bj-peano4  9389  bj-inf2vn  9404  bj-inf2vn2  9405
  Copyright terms: Public domain W3C validator