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  396  jcab  522  ioran  656  ordi  717  dfandc  766  stabtestimpdc  812  pm4.55dc  832  mpbi2and  836  mpbir2and  837  pm4.82  843  pm4.83dc  844  rnlem  869  syl22anc  1120  syl112anc  1123  syl121anc  1124  syl211anc  1125  syl23anc  1126  syl32anc  1127  syl122anc  1128  syl212anc  1129  syl221anc  1130  syl222anc  1135  syl123anc  1136  syl132anc  1137  syl213anc  1138  syl231anc  1139  syl312anc  1140  syl321anc  1141  syl223anc  1145  syl232anc  1146  syl322anc  1147  syl233anc  1148  syl323anc  1149  syl332anc  1150  ecased  1222  19.26  1346  nfand  1438  19.40  1500  equsexd  1595  sbcof2  1669  sbequ8  1705  eu2  1922  eu3h  1923  eu5  1925  mooran2  1951  datisi  1988  felapton  1992  darapti  1993  dimatis  1995  fresison  1996  fesapo  1998  r19.26  2415  r19.29af2  2426  r19.40  2438  eqvinc  2640  eqvincg  2641  reu6  2703  reu3  2704  indifdir  3166  undif3ss  3171  un00  3236  disjpr2  3404  prel12  3512  prneimg  3515  preqsn  3516  opexgOLD  3935  opth  3944  0nelop  3955  euotd  3961  opelopabsb  3967  ispod  4011  elon2  4058  unexb  4123  opeluu  4128  eusvnfb  4132  suc11g  4215  nlimsucg  4222  tfi  4228  vtoclr  4311  opthprc  4314  ideqg  4410  resiexg  4576  dminss  4661  imainss  4662  ssxpbm  4679  relrelss  4767  funopg  4856  fntpg  4877  fun11uni  4891  imain  4903  funimaexglem  4904  funssxp  4981  ffdm  4982  f00  5002  dffo2  5031  fodmrnu  5035  foco  5037  fun11iun  5068  f1o00  5082  fv3  5118  dff2  5232  dff3im  5233  dffo4  5236  ffnfv  5244  ffvresb  5249  fsn2  5258  fconstfvm  5300  fnfvima  5314  fcof1o  5350  isocnv  5372  isotr  5377  riotaprop  5411  acexmidlemcase  5427  caovlem2d  5612  f1ocnvd  5621  caofcom  5653  resfunexgALT  5656  elxp7  5716  2ndrn  5728  1stconst  5761  2ndconst  5762  cnvf1olem  5764  poxp  5771  dftpos4  5796  dfsmo2  5820  tfrlem5  5848  tfrlemiex  5862  rdgon  5889  frecabex  5895  frecrdg  5904  oawordi  5960  nnmordi  5996  iserd  6039  relelec  6053  erth  6057  qliftfun  6095  elni2  6168  dfplpq2  6207  dfmpq2  6208  enqbreq2  6210  enqdc1  6215  addcmpblnq  6220  addclnq  6228  nqpi  6231  addassnqg  6235  mulassnqg  6237  mulcanenq  6238  distrnqg  6240  1qec  6241  recex  6243  subhalfnqq  6265  enq0tr  6283  nqnq0pi  6287  nq0nn  6291  mulcanenq0ec  6294  nnnq0lem1  6295  addclnq0  6300  distrnq0  6308  addassnq0lemcl  6310  elnp1st2nd  6324  prarloc  6351  addlocprlemlt  6380  addlocprlemeq  6382  addlocprlemgt  6383  addclpr  6386  nqprm  6391  mullocprlem  6408  mullocpr  6409  mulclpr  6410  ltpopr  6426  ltaddpr  6428  ltexprlemm  6431  ltexprlemopl  6432  ltexprlemopu  6434  ltexprlemrnd  6436  ltexprlemdisj  6437  addcanprleml  6445  addcanprlemu  6446  addcanprg  6447  recexprlemm  6452  recexprlemopl  6453  recexprlemopu  6455  recexprlemrnd  6457  recexprlemdisj  6458  prsrlem1  6483  mulclsr  6495  mulasssrg  6499  distrsrg  6500  elreal2  6536  axmulass  6561  axdistr  6562  mullt0  7058  bdop  7241  bdunexb  7282  bj-om  7298  findset  7306  bj-peano4  7316  bj-inf2vn  7331  bj-inf2vn2  7332
  Copyright terms: Public domain W3C validator