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

Theorem simp2d 1012
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp2d  |-  ( ph  ->  ch )

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp2 1000 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
31, 2syl 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  simp2bi  1015  erinxp  6636  resixp  6760  exmidapne  7290  addcanprleml  7644  addcanprlemu  7645  ltmprr  7672  lelttrdi  8414  ixxdisj  9935  ixxss1  9936  ixxss2  9937  ixxss12  9938  iccgelb  9964  iccss2  9976  icodisj  10024  ioom  10293  elicore  10299  flqdiv  10354  mulqaddmodid  10397  modsumfzodifsn  10429  addmodlteq  10431  immul  10923  sumtp  11457  crth  12259  phimullem  12260  eulerthlem1  12262  eulerthlema  12265  eulerthlemh  12266  eulerthlemth  12267  ctiunct  12494  structn0fun  12528  strleund  12618  strext  12620  mhmlin  12934  subm0cl  12945  eqger  13180  eqgcpbl  13184  lmodvsdi  13644  lss0cl  13702  rnglidlmsgrp  13830  2idlcpblrng  13855  lmcl  14222  lmtopcnp  14227  xmeter  14413  tgqioo  14524  ivthinclemlopn  14591  ivthinclemuopn  14593  limcimolemlt  14610  limcresi  14612  limccnpcntop  14621  limccnp2lem  14622  limccnp2cntop  14623  cosordlem  14747
  Copyright terms: Public domain W3C validator