Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm5.32i | Structured version Visualization version GIF version |
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
pm5.32i.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
pm5.32i | ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.32i.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | pm5.32 666 | . 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: pm5.32ri 668 biadan2 672 anbi2i 726 abai 832 anabs5 847 pm5.33 918 cases 1004 equsexvw 1919 equsexv 2095 equsexALT 2282 2sb5rf 2439 2eu8 2548 eq2tri 2671 rexbiia 3022 reubiia 3104 rmobiia 3109 rabbiia 3161 ceqsrexbv 3307 euxfr 3359 2reu5 3383 dfpss3 3655 eldifpr 4152 eldiftp 4175 eldifsn 4260 elrint 4453 elriin 4529 reuxfrd 4819 opeqsn 4892 rabxp 5078 copsex2gb 5153 eliunxp 5181 restidsing 5377 ressn 5588 dflim2 5698 fncnv 5876 dff1o5 6059 respreima 6252 dff4 6281 dffo3 6282 f1ompt 6290 fsn 6308 fconst3 6382 fconst4 6383 eufnfv 6395 dff13 6416 f1mpt 6419 isocnv3 6482 isores2 6483 isoini 6488 eloprabga 6645 mpt2mptx 6649 resoprab 6654 elrnmpt2res 6672 ov6g 6696 dfwe2 6873 dflim3 6939 dflim4 6940 dfopab2 7113 dfoprab3s 7114 dfoprab3 7115 fparlem1 7164 fparlem2 7165 brtpos2 7245 dftpos3 7257 tpostpos 7259 dfsmo2 7331 dfrecs3 7356 tz7.48-1 7425 ondif1 7468 ondif2 7469 elixp2 7798 mapsnen 7920 xpcomco 7935 eqinf 8273 infempty 8295 r0weon 8718 isinfcard 8798 dfac5lem1 8829 fpwwe 9347 axgroth6 9529 axgroth3 9532 elni2 9578 indpi 9608 recmulnq 9665 genpass 9710 lemul1a 10756 sup3 10859 elnn0z 11267 elznn0 11269 elznn 11270 eluz2b1 11635 eluz2b3 11638 elfz2nn0 12300 elfzo3 12355 shftidt2 13669 clim0 14085 fprod2dlem 14549 divalglem4 14957 ndvdsadd 14972 gcdaddmlem 15083 algfx 15131 isprm3 15234 isprm5 15257 isprm7 15258 xpsfrnel 16046 isacs2 16137 isfull2 16394 isfth2 16398 tosso 16859 odudlatb 17019 nsgacs 17453 isgim2 17530 isabl2 18024 iscyg3 18111 iscrng2 18386 isdrng2 18580 drngprop 18581 islmim2 18887 islpir2 19072 isnzr2 19084 iunocv 19844 ishil2 19882 islinds2 19971 ssntr 20672 isclo2 20702 isperf2 20766 isperf3 20767 nrmsep3 20969 iscon2 21027 iskgen3 21162 ptpjpre1 21184 tx1cn 21222 tx2cn 21223 hausdiag 21258 qustgplem 21734 istdrg2 21791 isngp2 22211 isngp3 22212 isnvc2 22313 isclmp 22705 iscvs 22735 isncvsngp 22757 ovoliunlem1 23077 ismbl2 23102 i1f1lem 23262 i1fres 23278 itg1climres 23287 pilem1 24009 ellogrn 24110 ellogdm 24185 1cubr 24369 atandm 24403 atandm2 24404 atandm3 24405 atandm4 24406 atans2 24458 eldmgm 24548 isph 27061 h2hcau 27220 h2hlm 27221 issh2 27450 isch2 27464 h1dei 27793 elbdop2 28114 dfadj2 28128 cnvadj 28135 hhcno 28147 hhcnf 28148 eleigvec2 28201 riesz2 28309 rnbra 28350 elat2 28583 ofpreima 28848 mpt2mptxf 28860 f1od2 28887 maprnin 28894 xrofsup 28923 xrdifh 28932 cmpcref 29245 ofcfval 29487 ispisys2 29543 1stmbfm 29649 2ndmbfm 29650 eulerpartlems 29749 eulerpartlemgc 29751 eulerpartlemv 29753 eulerpartlemd 29755 eulerpartlemr 29763 eulerpartlemn 29770 ballotlemodife 29886 sgn3da 29930 bnj945 30098 bnj1172 30323 bnj1296 30343 snmlval 30567 dfres3 30902 eldm3 30905 nofulllem5 31105 brtxp2 31158 brpprod3a 31163 dffun10 31191 elfuns 31192 brimg 31214 dfrdg4 31228 ellines 31429 opnrebl 31485 bj-ax12ig 31802 bj-equsexval 31827 bj-csbsnlem 32090 bj-mpt2mptALT 32253 bj-elid3 32264 bj-eldiag 32268 taupilem3 32342 topdifinffinlem 32371 relowlssretop 32387 istotbnd3 32740 isbnd2 32752 isbnd3b 32754 exidcl 32845 isdrngo2 32927 isdrngo3 32928 iscrngo2 32966 isdmn2 33024 isfldidl2 33038 isdmn3 33043 islshpat 33322 iscvlat2N 33629 ishlat3N 33659 snatpsubN 34054 diclspsn 35501 isnacs2 36287 islnm2 36666 islnr2 36703 islnr3 36704 issdrg2 36787 isdomn3 36801 elinintab 36900 elmapintab 36921 elinlem 36923 cnvcnvintabd 36925 k0004lem1 37465 dffo3f 38359 2reu8 39841 dfdfat2 39860 isodd2 40086 iseven5 40114 isodd7 40115 oddprmne2 40162 isfusgrcl 40540 iscusgrvtx 40643 iscusgredg 40645 ismhm0 41595 sgrp2sgrp 41654 0ringdif 41660 isrnghmmul 41683 eliunxp2 41905 mpt2mptx2 41906 elbigo 42143 |
Copyright terms: Public domain | W3C validator |