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

Theorem anim12i 321
Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
Hypotheses
Ref Expression
anim12i.1 (φψ)
anim12i.2 (χθ)
Assertion
Ref Expression
anim12i ((φ χ) → (ψ θ))

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2 (φψ)
2 anim12i.2 . 2 (χθ)
3 id 19 . 2 ((ψ θ) → (ψ θ))
41, 2, 3syl2an 273 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-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  anim12ci  322  anim1i  323  anim2i  324  hban  1436  sbimi  1644  spsbbi  1722  2exeu  1989  cgsex2g  2584  cgsex4g  2585  spc2egv  2636  spc2gv  2637  sseq2  2961  unssin  3170  uneqin  3182  undif3ss  3192  prneimg  3536  ssunieq  3604  iuneq1  3661  iuneq2  3664  copsex2t  3973  soeq2  4044  tpexg  4145  eldifpw  4174  iunpw  4177  peano5  4264  opbrop  4362  xpsspw  4393  coeq1  4436  coeq2  4437  cnveq  4452  dmeq  4478  sotri  4663  elxp4  4751  elxp5  4752  funun  4887  funtp  4895  imain  4924  2elresin  4953  funssxp  5003  fssres  5009  f1co  5044  foun  5088  resdif  5091  f1oco  5092  fvun1  5182  fvreseq  5214  ftpg  5290  f1o2ndf1  5791  smores  5848  nnaord  6018  nnm00  6038  brecop  6132  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  th3q  6147  addcmpblnq  6351  mulcmpblnq  6352  mulclnq  6360  dmaddpq  6363  dmmulpq  6364  mulcanenq  6369  distrnqg  6371  ltdcnq  6381  ltexnqq  6391  enq0breq  6419  mulcmpblnq0  6427  mulcanenq0ec  6428  addnnnq0  6432  mulnnnq0  6433  mulclnq0  6435  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  distrnq0  6442  elinp  6457  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  addnqprl  6512  addnqpru  6513  distrlem1prl  6558  distrlem1pru  6559  ltsopr  6570  cauappcvgprlemdisj  6623  caucvgprlemdisj  6645  addcmpblnr  6667  addsrpr  6673  mulsrpr  6674  addclsr  6681  addasssrg  6684  0idsr  6695  1idsr  6696  00sr  6697  mulgt0sr  6704  axaddcl  6750  axmulcl  6752  axaddass  6756  axdistr  6758  cnegexlem3  6985  cnegex  6986  apirr  7389  recexaplem2  7415  zletric  8065  zlelttric  8066  qaddcl  8346  qmulcl  8348  qreccl  8351  iccss  8580  fzsubel  8693  elfz0add  8749  difelfznle  8763  2ffzeq  8768  fzonmapblen  8813  ubmelfzo  8826  ubmelm1fzo  8852  mulexp  8948  mulexpzap  8949  leexp1a  8963  bj-indind  9391  peano5setOLD  9400
  Copyright terms: Public domain W3C validator