Theorem con1bid 345

Description: A contraposition deduction. (Contributed by NM, 9-Oct-1999.)

Hypothesis

Ref	Expression
con1bid.1	|- ( ph -> ( -. ps <-> ch ) )

Assertion

Ref	Expression
con1bid	|- ( ph -> ( -. ch <-> ps ) )

Proof of Theorem con1bid

Step	Hyp	Ref	Expression
1		con1bid.1	. . . 4 |- ( ph -> ( -. ps <-> ch ) )
2	1	bicomd 213	. . 3 |- ( ph -> ( ch <-> -. ps ) )
3	2	con2bid 344	. 2 |- ( ph -> ( ps <-> -. ch ) )
4	3	bicomd 213	1 |- ( ph -> ( -. ch <-> ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  pm5.18  371  necon1bbid  2833  r19.9rzv  4065  onmindif  5815  iotanul  5866  ondif2  7582  cnpart  13980  sadadd2lem2  15172  isnirred  18700  isreg2  21181  kqcldsat  21536  trufil  21714  itg2cnlem2  23529  issqf  24862  eupth2lem3lem4  27091  pjnorm2  28586  atdmd  29257  atmd2  29259  dfrdg4  32058  dalawlem13  35169