Theorem 3simp1d 792

Description: Deduce a conjunct from a triple conjunction.

Hypothesis

Ref	Expression
3simp1d.1	|- (ph -> (ps /\ ch /\ th))

Assertion

Ref	Expression
3simp1d	|- (ph -> ps)

Proof of Theorem 3simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- (ph -> (ps /\ ch /\ th))
2		3simp1 786	. 2 |- ((ps /\ ch /\ th) -> ps)
3	1, 2	syl 10	1 |- (ph -> ps)

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  iccssret 6329  ioossicc 6330  icoshftf1oi 6342  climaddlem3 7052  climmullem8 7063  isumcmpi 7150  ivthlem6 7221  ivthlem7 7222  ivthlem4OLD 7228  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthOLD 7233  ivth2OLD 7234  abspef01tlub 7336  efcnlem2 7360  reeff1olem1 7364  reeff1olem1OLD 7366  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  sin01gt0 7418  cos01gt0 7419  sin02gt0 7420  grpfo 7977  subgres 8054  subgid 8057  vcabl 8113  nvvc 8174  pilem2 8591  efif 8636  efifolem4 8640  efifolem7 8643  efif1lem3 8647  efif1lem4 8648  circgrp 8660  shftefif1olem 8661  shftefif1olemOLD 8662  effoi 8666  effoiOLD 8667  eleigvecclt 9799  ghomgrplem 10294  hmeomap 10405  filesn 10434  filusb 10436  doma 10505  dedalg 10520  cmpmorp 10556  ehm 10563  vidfunid 10595

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775

Copyright terms: Public domain