Theorem con34b 292

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

Assertion

Ref	Expression
con34b

Proof of Theorem con34b

Step	Hyp	Ref	Expression
1		con3 134	. 2
2		ax-3 8	. 2
3	1, 2	impbii 188	1

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

This theorem is referenced by:  mtt  339  pm4.14  578  r19.23v  2937  raldifsni  4160  dff14a  6177  weniso  6250  dfom2  6702  dfsup2  7922  wemapsolem  7996  pwfseqlem3  9059  indstr  11179  rpnnen2  13959  algcvgblem  14206  isirred2  17350  isdomn2  17948  ist0-3  19846  mdegleb  22464  dchrelbas4  23518  toslublem  27655  tosglblem  27657  tsbi3  30542  isdomn3  31164  conss34  31351  aacllem  33216

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 185