Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iman | Structured version Visualization version GIF version |
Description: Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.) |
Ref | Expression |
---|---|
iman | ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 304 | . . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓) | |
2 | 1 | imbi2i 326 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ¬ ¬ 𝜓)) |
3 | imnan 438 | . 2 ⊢ ((𝜑 → ¬ ¬ 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
4 | 2, 3 | bitri 264 | 1 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 |
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 df-an 386 |
This theorem is referenced by: annim 441 pm3.24 926 xor 935 nic-mpALT 1597 nic-axALT 1599 rexanali 2998 difdif 3736 dfss4 3858 difin 3861 ssdif0 3942 difin0ss 3946 inssdif0 3947 npss0OLD 4015 dfif2 4088 notzfaus 4840 dffv2 6271 tfinds 7059 domtriord 8106 inf3lem3 8527 nominpos 11269 isprm3 15396 vdwlem13 15697 vdwnn 15702 psgnunilem4 17917 efgredlem 18160 efgred 18161 ufinffr 21733 ptcmplem5 21860 nmoleub2lem2 22916 ellogdm 24385 pntpbnd 25277 cvbr2 29142 cvnbtwn2 29146 cvnbtwn3 29147 cvnbtwn4 29148 chpssati 29222 chrelat2i 29224 chrelat3 29230 bnj1476 30917 bnj110 30928 bnj1388 31101 df3nandALT1 32396 imnand2 32399 bj-andnotim 32573 lindsenlbs 33404 poimirlem11 33420 poimirlem12 33421 fdc 33541 lpssat 34300 lssat 34303 lcvbr2 34309 lcvbr3 34310 lcvnbtwn2 34314 lcvnbtwn3 34315 cvrval2 34561 cvrnbtwn2 34562 cvrnbtwn3 34563 cvrnbtwn4 34566 atlrelat1 34608 hlrelat2 34689 dihglblem6 36629 or3or 38319 uneqsn 38321 plvcofphax 41114 |
Copyright terms: Public domain | W3C validator |