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  6499  genpmu  6500  genprndl  6503  genprndu  6504  addnqprl  6511  addnqpru  6512  distrlem1prl  6557  distrlem1pru  6558  ltsopr  6569  cauappcvgprlemdisj  6622  addcmpblnr  6647  addsrpr  6653  mulsrpr  6654  addclsr  6661  addasssrg  6664  0idsr  6675  1idsr  6676  00sr  6677  mulgt0sr  6684  axaddcl  6730  axmulcl  6732  axaddass  6736  axdistr  6738  cnegexlem3  6965  cnegex  6966  apirr  7369  recexaplem2  7395  zletric  8045  zlelttric  8046  qaddcl  8326  qmulcl  8328  qreccl  8331  iccss  8560  fzsubel  8673  elfz0add  8729  difelfznle  8743  2ffzeq  8748  fzonmapblen  8793  ubmelfzo  8806  ubmelm1fzo  8832  mulexp  8928  mulexpzap  8929  leexp1a  8943  peano5set  9374
  Copyright terms: Public domain W3C validator