Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem iman 237

Description: Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176.

Assertion

Ref	Expression
iman

---

Proof of Theorem iman

Step	Hyp	Ref	Expression
1		pm4.13 161	. . 3
2	1	imbi2i 185	. 2
3		df-an 225	. . 3
4	3	con2bii 221	. 2
5	2, 4	bitr 173	1

Colors of variables: wff set class

Syntax hints:   wn 2   wi 3   wb 146   wa 223

This theorem is referenced by:  annim 238  pm3.37 286  pm4.14 352  dfbi 668  nicodraw 949  nicodmpraw 950  exanali 1039  dfpss3 2124  difdif 2156  dfss4 2232  ssdif0 2317  difin0ss 2322  inssdif0 2323  dfif2 2353  notzfaus 2731  inf3lem3 4587  nominpos 5990  cvbr2t 10120  cvnbtwn2t 10124  cvnbtwn3t 10125  cvnbtwn4t 10126  chpssat 10198  chrelat2 10200  chrelat3t 10206

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain