Theorem con34b 306

Description: A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.)

Assertion

Ref	Expression
con34b	|- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )

Proof of Theorem con34b

Step	Hyp	Ref	Expression
1		con3 149	. 2 |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
2		con4 112	. 2 |- ( ( -. ps -> -. ph ) -> ( ph -> ps ) )
3	1, 2	impbii 199	1 |- ( ( ph -> ps ) <-> ( -. ps -> -. ph ) )

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:  mtt  354  pm4.14  602  dfbi3  994  19.23t  2079  19.23tOLD  2218  r19.23v  3023  raldifsni  4324  dff14a  6527  weniso  6604  dfom2  7067  dfsup2  8350  wemapsolem  8455  pwfseqlem3  9482  indstr  11756  rpnnen2lem12  14954  algcvgblem  15290  isirred2  18701  isdomn2  19299  ist0-3  21149  mdegleb  23824  dchrelbas4  24968  toslublem  29667  tosglblem  29669  poimirlem25  33434  poimirlem30  33439  tsbi3  33942  isdomn3  37782  ntrneikb  38392  conss34OLD  38646  aacllem  42547