Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm4.71ri | Structured version Visualization version GIF version |
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
Ref | Expression |
---|---|
pm4.71ri.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
pm4.71ri | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71ri.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | pm4.71r 661 | . 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑))) | |
3 | 1, 2 | mpbi 219 | 1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: biadan2 672 anabs7 848 orabs 896 prlem2 998 eu5 2484 2moswap 2535 exsnrex 4168 eliunxp 5181 asymref 5431 dffun9 5832 funcnv 5872 funcnv3 5873 f1ompt 6290 eufnfv 6395 dff1o6 6431 dfom2 6959 elxp4 7003 elxp5 7004 abexex 7042 dfoprab4 7116 tpostpos 7259 brwitnlem 7474 erovlem 7730 elixp2 7798 xpsnen 7929 elom3 8428 cardval2 8700 isinfcard 8798 infmap2 8923 elznn0nn 11268 zrevaddcl 11299 qrevaddcl 11686 hash2prb 13111 cotr2g 13563 climreu 14135 isprm3 15234 hashbc0 15547 imasleval 16024 isssc 16303 isgim 17527 eldprd 18226 brric2 18568 islmim 18883 tgval2 20571 eltg2b 20574 snfil 21478 isms2 22065 setsms 22095 elii1 22542 phtpcer 22602 phtpcerOLD 22603 elovolm 23050 ellimc2 23447 limcun 23465 1cubr 24369 fsumvma2 24739 dchrelbas3 24763 2lgslem1b 24917 rusgranumwlks 26483 isgrpo 26735 mdsl2i 28565 cvmdi 28567 rabfmpunirn 28833 eulerpartlemn 29770 bnj580 30237 bnj1049 30296 snmlval 30567 elmthm 30727 brtxp2 31158 brpprod3a 31163 ismgmOLD 32819 prtlem100 33161 islln2 33815 islpln2 33840 islvol2 33884 elmapintrab 36901 clcnvlem 36949 rusgrnumwwlks 41177 eliunxp2 41905 elbigo 42143 |
Copyright terms: Public domain | W3C validator |