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  935  pm5.63dc  936  simplbi2com  1432  reuss2  3401  elni2  7251  elpq  9582  elfz0ubfz0  10056  elfzmlbp  10063  fzo1fzo0n0  10114  elfzo0z  10115  fzofzim  10119  elfzodifsumelfzo  10132  p1modz1  11730  dfgcd2  11943  algcvga  11979  pcprendvds  12218