Theorem bicon2i 194

Description: A contraposition inference.

Hypothesis

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

Assertion

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

Proof of Theorem bicon2i

Step	Hyp	Ref	Expression
1		bicon2.1	. . . 4 |- (ph <-> -. ps)
2	1	bicomi 150	. . 3 |- (-. ps <-> ph)
3	2	bicon1i 193	. 2 |- (-. ph <-> ps)
4	3	bicomi 150	1 |- (ps <-> -. ph)

Syntax hints:  -. wn 1   <-> wb 127

This theorem is referenced by:  iman 205  annim 206  imnan 207  pm5.18 497  nbbn 498  alnex 716  exnal 721  exanali 725  19.35 754  19.41 774  eqs3 830  eqsex 834  sb5y 883  dfral2 1211  dfrex2 1212  r19.35 1298  sbc2or 1454  ddif 1597  dfun2 1668  dfin2 1669  dfnul2 1709  noel 1711  disj4 1737  supmo 2156  onuninsuc 2356  intirr 2628  alephgeom 3687  reclem2pr 3951  letri 4306  nn0ltp1let 4556  halfnz 4586  zltp1let 4597  nneo 4719  infdif 4948

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

This theorem depends on definitions:  df-bi 128

metamath.org