Theorem simplbi2 385

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 133	. 2 |- ( ( ps /\ ch ) -> ph )
3	2	ex 115	1 |- ( ps -> ( ch -> ph ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.62dc  954  pm5.63dc  955  simplbi2com  1490  reuss2  3501  elni2  7629  elpq  9981  elfz0ubfz0  10459  elfzmlbp  10466  fzo1fzo0n0  10522  elfzo0z  10523  fzofzim  10527  elfzodifsumelfzo  10546  swrdswrd  11397  swrdccatin1  11417  p1modz1  12480  dfgcd2  12710  algcvga  12748  pcprendvds  12988  usgruspgrben  16181  trlf1  16383