Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  anim12d Unicode version

Theorem anim12d 333
 Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
Hypotheses
Ref Expression
anim12d.1
anim12d.2
Assertion
Ref Expression
anim12d

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2
2 anim12d.2 . 2
3 idd 21 . 2
41, 2, 3syl2and 293 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  anim1d  334  anim2d  335  anim12  342  im2anan9  588  anim12dan  590  3anim123d  1298  hband  1466  hbbid  1555  spsbim  1816  moim  2064  moimv  2066  2euswapdc  2091  rspcimedv  2795  soss  4244  trin2  4938  xp11m  4985  funss  5150  fun  5303  dff13  5677  f1eqcocnv  5700  isores3  5724  isosolem  5733  f1o2ndf1  6133  tposfn2  6171  tposf1o2  6175  nndifsnid  6411  nnaordex  6431  supmoti  6888  isotilem  6901  recexprlemss1l  7468  recexprlemss1u  7469  caucvgsrlemoffres  7633  suplocsrlem  7641  nnindnn  7726  eqord1  8270  lemul12b  8644  lt2msq  8669  lbreu  8728  cju  8744  nnind  8761  uz11  9373  xrre2  9635  ico0  10071  ioc0  10072  expcan  10495  gcdaddm  11709  bezoutlemaz  11728  bezoutlembz  11729  isprm3  11836  epttop  12299  cnptopresti  12447  cnptoprest  12448  txcnp  12480  addcncntoplem  12760  mulcncflem  12799  bj-stand  13128  exmidsbthrlem  13393
 Copyright terms: Public domain W3C validator