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

Theorem anim12i 338
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 289 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  anim12ci  339  anim1i  340  anim2i  342  hban  1547  sbimi  1764  spsbbi  1844  2exeu  2118  cgsex2g  2773  cgsex4g  2774  spc2egv  2827  spc2gv  2828  sseq2  3179  unssin  3374  uneqin  3386  undif3ss  3396  prneimg  3772  ssunieq  3840  iuneq1  3897  iuneq2  3900  copsex2t  4242  soeq2  4313  tpexg  4441  eldifpw  4474  iunpw  4477  peano5  4594  opbrop  4702  xpsspw  4735  coeq1  4780  coeq2  4781  cnveq  4797  dmeq  4823  sotri  5020  elxp4  5112  elxp5  5113  funun  5256  funtp  5265  imain  5294  2elresin  5323  funssxp  5381  fssres  5387  f1co  5429  foun  5476  resdif  5479  f1oco  5480  fvun1  5578  elfvmptrab1  5606  fvreseq  5615  ftpg  5696  f1o2ndf1  6223  spc2ed  6228  smores  6287  nnaord  6504  nnm00  6525  brecop  6619  eroveu  6620  ecopovtrn  6626  ecopovtrng  6629  th3qlem1  6631  th3q  6634  ixpeq2  6706  djuexb  7037  addcmpblnq  7357  mulcmpblnq  7358  mulclnq  7366  dmaddpq  7369  dmmulpq  7370  mulcanenq  7375  distrnqg  7377  ltdcnq  7387  ltexnqq  7398  enq0breq  7426  mulcmpblnq0  7434  mulcanenq0ec  7435  addnnnq0  7439  mulnnnq0  7440  mulclnq0  7442  nqpnq0nq  7443  nqnq0a  7444  nqnq0m  7445  distrnq0  7449  elinp  7464  genpml  7507  genpmu  7508  genprndl  7511  genprndu  7512  addnqprl  7519  addnqpru  7520  distrlem1prl  7572  distrlem1pru  7573  ltsopr  7586  cauappcvgprlemdisj  7641  caucvgprlemdisj  7664  caucvgprprlemdisj  7692  addcmpblnr  7729  addsrpr  7735  mulsrpr  7736  addclsr  7743  addasssrg  7746  0idsr  7757  1idsr  7758  00sr  7759  mulgt0sr  7768  axaddcl  7854  axmulcl  7856  axaddass  7862  axdistr  7864  cnegexlem3  8124  cnegex  8125  apirr  8552  recexaplem2  8598  zletric  9286  zlelttric  9287  difgtsumgt  9311  qaddcl  9624  qmulcl  9626  qreccl  9631  iccss  9928  fzsubel  10046  elfz0add  10106  difelfznle  10121  2ffzeq  10127  fzonmapblen  10173  ubmelfzo  10186  ubmelm1fzo  10212  subfzo0  10228  qletric  10230  qlelttric  10231  adddivflid  10278  mulexp  10545  mulexpzap  10546  leexp1a  10561  faclbnd  10705  rexanuz  10981  sqabsadd  11048  sqabssub  11049  abs2dif  11099  rpmincl  11230  xrminrpcl  11266  fsum2dlemstep  11426  fprodeq0  11609  fprod2dlemstep  11614  summodnegmod  11813  dvds2ln  11815  dvdsflip  11840  gcdsupex  11941  gcdsupcl  11942  gcdabs  11972  sqgcd  12013  nnwosdc  12023  lcmabs  12059  lcmgcdlem  12060  lcmgcd  12061  lcmgcdeq  12066  qredeq  12079  cncongr1  12086  cncongr2  12087  hashgcdlem  12221  dvdsprmpweqle  12319  difsqpwdvds  12320  mndissubm  12756  tgcl  13231  uncld  13280  innei  13330  cnco  13388  txbas  13425  txbasval  13434  blin2  13599  qtopbasss  13688  lgsmulsqcoprm  14114  bj-charfunbi  14219  bj-indind  14340
  Copyright terms: Public domain W3C validator