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  1421  sbimi  1629  spsbbi  1707  2exeu  1974  cgsex2g  2567  cgsex4g  2568  spc2egv  2619  spc2gv  2620  sseq2  2944  unssin  3153  uneqin  3165  undif3ss  3175  prneimg  3519  ssunieq  3587  iuneq1  3644  iuneq2  3647  copsex2t  3956  soeq2  4027  tpexg  4129  eldifpw  4158  iunpw  4161  peano5  4248  opbrop  4346  xpsspw  4377  coeq1  4420  coeq2  4421  cnveq  4436  dmeq  4462  sotri  4647  elxp4  4735  elxp5  4736  funun  4870  funtp  4878  imain  4907  2elresin  4936  funssxp  4985  fssres  4991  f1co  5026  foun  5070  resdif  5073  f1oco  5074  fvun1  5164  fvreseq  5196  ftpg  5272  f1o2ndf1  5772  smores  5829  nnaord  5993  nnm00  6013  brecop  6107  eroveu  6108  ecopovtrn  6114  ecopovtrng  6117  th3qlem1  6119  th3q  6122  addcmpblnq  6226  mulcmpblnq  6227  mulclnq  6235  dmaddpq  6238  dmmulpq  6239  mulcanenq  6244  distrnqg  6246  ltdcnq  6256  ltexnqq  6266  enq0breq  6291  mulcmpblnq0  6299  mulcanenq0ec  6300  addnnnq0  6304  mulnnnq0  6305  mulclnq0  6307  nqpnq0nq  6308  nqnq0a  6309  nqnq0m  6310  distrnq0  6314  elinp  6328  genpml  6372  genpmu  6373  genprndl  6376  genprndu  6377  addnqprl  6384  addnqpru  6385  distrlem1prl  6421  distrlem1pru  6422  ltsopr  6433  addcmpblnr  6486  addsrpr  6492  mulsrpr  6493  addclsr  6500  addasssrg  6503  0idsr  6514  1idsr  6515  00sr  6516  mulgt0sr  6522  axaddcl  6560  axmulcl  6562  axaddass  6566  axdistr  6568  cnegexlem3  6781  cnegex  6782  peano5set  7309
  Copyright terms: Public domain W3C validator