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  953  pm5.63dc  954  simplbi2com  1489  reuss2  3487  elni2  7534  elpq  9883  elfz0ubfz0  10360  elfzmlbp  10367  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzodifsumelfzo  10447  swrdswrd  11290  swrdccatin1  11310  p1modz1  12373  dfgcd2  12603  algcvga  12641  pcprendvds  12881  usgruspgrben  16056  trlf1  16258