Theorem simplbi2 383

Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)

Hypothesis

Ref	Expression
pm3.26bi2.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
simplbi2	|- ( ps -> ( ch -> ph ) )

Proof of Theorem simplbi2

Step	Hyp	Ref	Expression
1		pm3.26bi2.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
2	1	biimpri 132	. 2 |- ( ( ps /\ ch ) -> ph )
3	2	ex 114	1 |- ( ps -> ( ch -> ph ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.62dc  940  pm5.63dc  941  simplbi2com  1437  reuss2  3407  elni2  7276  elpq  9607  elfz0ubfz0  10081  elfzmlbp  10088  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzodifsumelfzo  10157  p1modz1  11756  dfgcd2  11969  algcvga  12005  pcprendvds  12244