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  3424  prel12  3532  prneimg  3535  preqsn  3536  opexgOLD  3955  opth  3964  0nelop  3975  euotd  3981  opelopabsb  3987  ispod  4031  elon2  4078  unexb  4142  opeluu  4147  eusvnfb  4151  suc11g  4234  nlimsucg  4241  tfi  4247  vtoclr  4330  opthprc  4333  ideqg  4429  resiexg  4595  dminss  4680  imainss  4681  ssxpbm  4698  relrelss  4786  funopg  4875  fntpg  4896  fun11uni  4910  imain  4922  funimaexglem  4923  funssxp  5001  ffdm  5002  f00  5022  dffo2  5051  fodmrnu  5055  foco  5057  fun11iun  5088  f1o00  5102  fv3  5138  dff2  5252  dff3im  5253  dffo4  5256  ffnfv  5264  ffvresb  5269  fsn2  5278  fconstfvm  5320  fnfvima  5334  fcof1o  5370  isocnv  5392  isotr  5397  riotaprop  5431  acexmidlemcase  5447  caovlem2d  5632  f1ocnvd  5641  caofcom  5673  resfunexgALT  5676  elxp7  5736  2ndrn  5748  1stconst  5781  2ndconst  5782  cnvf1olem  5784  poxp  5791  dftpos4  5816  dfsmo2  5840  tfrlem5  5868  tfrlemiex  5883  rdgon  5910  frecabex  5917  frecrdg  5925  oawordi  5981  nntri3  6007  nnmordi  6018  iserd  6061  relelec  6075  erth  6079  qliftfun  6117  bren  6157  elni2  6291  dfplpq2  6331  dfmpq2  6332  enqbreq2  6334  enqdc1  6339  addcmpblnq  6344  addclnq  6352  nqpi  6355  addassnqg  6359  mulassnqg  6361  mulcanenq  6362  distrnqg  6364  1qec  6365  recexnq  6367  subhalfnqq  6390  enq0tr  6409  nqnq0pi  6413  nq0nn  6417  mulcanenq0ec  6420  nnnq0lem1  6421  addclnq0  6426  distrnq0  6434  addassnq0lemcl  6436  elnp1st2nd  6451  prarloc  6478  addlocprlemlt  6507  addlocprlemeq  6509  addlocprlemgt  6510  addclpr  6513  nqprm  6518  mullocprlem  6541  mullocpr  6542  mulclpr  6543  ltpopr  6559  ltaddpr  6561  ltexprlemm  6564  ltexprlemopl  6565  ltexprlemopu  6567  ltexprlemrnd  6569  ltexprlemdisj  6570  addcanprleml  6578  addcanprlemu  6579  addcanprg  6580  recexprlemm  6586  recexprlemopl  6587  recexprlemopu  6589  recexprlemrnd  6591  recexprlemdisj  6592  prsrlem1  6622  mulclsr  6634  mulasssrg  6638  distrsrg  6639  elreal2  6680  axmulass  6709  axdistr  6710  add20  7216  mullt0  7222  rereim  7322  ltmul1  7328  cru  7338  mulap0r  7351  divmuldivap  7422  divmuleqap  7427  divadddivap  7437  ltmul12a  7558  lemul12a  7560  lemulge11  7564  lediv12a  7592  lediv2a  7593  recgt1i  7596  recreclt  7598  ledivp1  7601  lemul1ad  7637  lemul2ad  7638  ltmul12ad  7639  lemul12ad  7640  lemul12bd  7641  nndivre  7681  nndivtr  7687  halfaddsubcl  7885  halfaddsub  7886  lt2halves  7887  nnrecl  7905  elnn0nn  7950  elnnnn0b  7952  elnnnn0c  7953  nn0addge1  7954  nn0addge2  7955  elnn0z  7984  elnnz1  7994  elz2  8038  zdivadd  8054  zdivmul  8055  zextle  8056  peano2uz2  8070  uzind  8074  btwnz  8082  uzss  8218  eluzp1m1  8221  eluz2b2  8265  qre  8285  qaddcl  8295  qmulcl  8297  qreccl  8300  irradd  8304  irrmul  8305  rprege0  8320  rprene0  8323  rpreap0  8324  rpcnne0  8325  rpcnap0  8326  rpregt0d  8351  rprege0d  8352  rprene0d  8353  rpcnne0d  8354  lediv2ad  8367  lediv12ad  8400  xrlttri3  8436  xrrebnd  8450  xrrege0  8456  elioo4g  8521  ioomax  8535  iccmax  8536  divelunit  8588  elfz5  8600  uzsubsubfz  8627  fzopth  8640  fzass4  8641  fzrev2  8663  uzsplit  8670  elfz2nn0  8689  difelfzle  8708  1fv  8712  4fvwrd4  8713  fzo1fzo0n0  8755  elfzom1elp1fzo  8774  bdop  8929  bdunexb  8970  bj-om  8990  findset  8998  bj-peano4  9008  bj-inf2vn  9023  bj-inf2vn2  9024
  Copyright terms: Public domain W3C validator