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  6418  mulcmpblnq0  6426  mulcanenq0ec  6427  addnnnq0  6431  mulnnnq0  6432  mulclnq0  6434  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  distrnq0  6441  elinp  6456  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  addnqprl  6512  addnqpru  6513  distrlem1prl  6556  distrlem1pru  6557  ltsopr  6568  addcmpblnr  6627  addsrpr  6633  mulsrpr  6634  addclsr  6641  addasssrg  6644  0idsr  6655  1idsr  6656  00sr  6657  mulgt0sr  6664  axaddcl  6710  axmulcl  6712  axaddass  6716  axdistr  6718  cnegexlem3  6945  cnegex  6946  apirr  7349  recexaplem2  7375  zletric  8025  zlelttric  8026  qaddcl  8306  qmulcl  8308  qreccl  8311  iccss  8540  fzsubel  8653  elfz0add  8709  difelfznle  8723  2ffzeq  8728  fzonmapblen  8773  ubmelfzo  8786  ubmelm1fzo  8812  mulexp  8908  mulexpzap  8909  leexp1a  8923  peano5set  9328
  Copyright terms: Public domain W3C validator