Theorem 3simp1d 806

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 800	. 2 |- ((ps /\ ch /\ th) -> ps)
3	1, 2	syl 10	1 |- (ph -> ps)

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  intfracq 6367  fldiv 6368  iccssre 6422  icoshftf1oii 6435  climaddlem3 7206  climmullem8 7217  isumcmpii 7305  ivthlem6 7376  ivthlem7 7377  abspef01tlubi 7486  efcnlem2 7511  reeff1olem1 7515  sin01bndlem2 7560  sin01bndlem3 7561  cos01bndlem2 7562  cos01bndlem3 7563  sin01gt0 7568  cos01gt0 7569  sin02gt0 7570  grpfo 8128  subgres 8201  subgid 8204  vcabl 8260  nvvc 8318  pilem2 8755  efif 8804  efifolem7 8811  efif1lem3 8815  efif1lem4 8816  circgrp 8823  shftefif1olem 8824  effoi 8828  eleigveccl 9966  ghomgrplem 10474  hmeomap 10612  filesn 10653  filusb 10655  doma 10743  dedalg 10758  cmpmorp 10794  ehm 10801  vidfunid 10841

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 154  df-an 232  df-3an 789

Copyright terms: Public domain