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  948  pm5.63dc  949  simplbi2com  1465  reuss2  3461  elni2  7462  elpq  9805  elfz0ubfz0  10282  elfzmlbp  10289  fzo1fzo0n0  10344  elfzo0z  10345  fzofzim  10349  elfzodifsumelfzo  10367  swrdswrd  11196  swrdccatin1  11216  p1modz1  12220  dfgcd2  12450  algcvga  12488  pcprendvds  12728