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

Theorem anim12i 325
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  |-  ( ph  ->  ps )
anim12i.2  |-  ( ch 
->  th )
Assertion
Ref Expression
anim12i  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2  |-  ( ph  ->  ps )
2 anim12i.2 . 2  |-  ( ch 
->  th )
3 id 19 . 2  |-  ( ( ps  /\  th )  ->  ( ps  /\  th ) )
41, 2, 3syl2an 277 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  anim12ci  326  anim1i  327  anim2i  328  hban  1455  sbimi  1663  spsbbi  1741  2exeu  2008  cgsex2g  2607  cgsex4g  2608  spc2egv  2659  spc2gv  2660  sseq2  2994  unssin  3203  uneqin  3215  undif3ss  3225  prneimg  3572  ssunieq  3640  iuneq1  3697  iuneq2  3700  copsex2t  4009  soeq2  4080  tpexg  4206  eldifpw  4235  iunpw  4238  peano5  4348  opbrop  4446  xpsspw  4477  coeq1  4520  coeq2  4521  cnveq  4536  dmeq  4562  sotri  4747  elxp4  4835  elxp5  4836  funun  4971  funtp  4979  imain  5008  2elresin  5037  funssxp  5087  fssres  5093  f1co  5128  foun  5172  resdif  5175  f1oco  5176  fvun1  5266  fvreseq  5298  ftpg  5374  f1o2ndf1  5876  spc2ed  5881  smores  5937  nnaord  6112  nnm00  6132  brecop  6226  eroveu  6227  ecopovtrn  6233  ecopovtrng  6236  th3qlem1  6238  th3q  6241  addcmpblnq  6522  mulcmpblnq  6523  mulclnq  6531  dmaddpq  6534  dmmulpq  6535  mulcanenq  6540  distrnqg  6542  ltdcnq  6552  ltexnqq  6563  enq0breq  6591  mulcmpblnq0  6599  mulcanenq0ec  6600  addnnnq0  6604  mulnnnq0  6605  mulclnq0  6607  nqpnq0nq  6608  nqnq0a  6609  nqnq0m  6610  distrnq0  6614  elinp  6629  genpml  6672  genpmu  6673  genprndl  6676  genprndu  6677  addnqprl  6684  addnqpru  6685  distrlem1prl  6737  distrlem1pru  6738  ltsopr  6751  cauappcvgprlemdisj  6806  caucvgprlemdisj  6829  caucvgprprlemdisj  6857  addcmpblnr  6881  addsrpr  6887  mulsrpr  6888  addclsr  6895  addasssrg  6898  0idsr  6909  1idsr  6910  00sr  6911  mulgt0sr  6919  axaddcl  6997  axmulcl  6999  axaddass  7003  axdistr  7005  cnegexlem3  7250  cnegex  7251  apirr  7669  recexaplem2  7706  zletric  8345  zlelttric  8346  qaddcl  8666  qmulcl  8668  qreccl  8673  iccss  8910  fzsubel  9024  elfz0add  9080  difelfznle  9094  2ffzeq  9099  fzonmapblen  9144  ubmelfzo  9157  ubmelm1fzo  9183  subfzo0  9198  qletric  9200  qlelttric  9201  adddivflid  9241  mulexp  9458  mulexpzap  9459  leexp1a  9474  faclbnd  9608  rexanuz  9814  sqabsadd  9881  sqabssub  9882  abs2dif  9932  summodnegmod  10137  dvds2ln  10139  dvdsflip  10162  bj-indind  10422  peano5setOLD  10431
  Copyright terms: Public domain W3C validator