![]() |
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 form). (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 569 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | mpbi 222 | 1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: pm5.32ri 571 anbi2i 616 anabs5 653 biadan2OLD 814 abai 818 annotanannot 825 pm5.33 826 cases 1026 equsexvw 2051 equsexv 2241 equsexALT 2383 2sb5rf 2529 2eu8 2688 eq2tri 2840 rexbiia 3222 reubiia 3314 rmobiia 3319 rabbiia 3380 ceqsrexbv 3539 euxfr 3603 2reu5 3632 dfpss3 3914 eldifpr 4425 eldiftp 4454 eldifsn 4549 elrint 4751 elriin 4826 reuxfrd 5132 opeqsnOLD 5200 rabxp 5400 copsex2gb 5477 eliunxp 5505 dfres3 5647 restidsing 5714 ressn 5925 dflim2 6032 fncnv 6207 dff1o5 6400 respreima 6608 dff4 6637 dffo3 6638 f1ompt 6645 fsn 6667 fconst3 6749 fconst4 6750 eufnfv 6763 dff13 6784 f1mpt 6790 isocnv3 6854 isores2 6855 isoini 6860 eloprabga 7024 mpt2mptx 7028 resoprab 7033 elrnmpt2res 7051 ov6g 7075 dfwe2 7259 dflim3 7325 dflim4 7326 dfopab2 7501 dfoprab3s 7502 dfoprab3 7503 fparlem1 7558 fparlem2 7559 brtpos2 7640 dftpos3 7652 tpostpos 7654 dfsmo2 7727 dfrecs3 7752 tz7.48-1 7821 ondif1 7865 ondif2 7866 elixp2 8198 xpcomco 8338 eqinf 8678 infempty 8701 r0weon 9168 isinfcard 9248 dfac5lem1 9279 fpwwe 9803 axgroth6 9985 axgroth3 9988 elni2 10034 indpi 10064 recmulnq 10121 genpass 10166 lemul1a 11231 sup3 11334 elnn0z 11741 elznn0 11743 elznn 11744 eluz2b1 12066 eluz2b3 12069 elfz2nn0 12749 elfzo3 12805 shftidt2 14228 clim0 14645 fprod2dlem 15113 divalglem4 15526 ndvdsadd 15540 gcdaddmlem 15651 algfx 15699 isprm3 15801 isprm5 15823 isprm7 15824 xpsfrnel 16609 isacs2 16699 isfull2 16956 isfth2 16960 tosso 17422 odudlatb 17582 nsgacs 18014 isgim2 18091 isabl2 18587 iscyg3 18674 iscrng2 18950 isdrng2 19149 drngprop 19150 islmim2 19461 islpir2 19648 isnzr2 19660 iunocv 20424 ishil2 20462 islinds2 20556 ssntr 21270 isclo2 21300 isperf2 21364 isperf3 21365 nrmsep3 21567 isconn2 21626 iskgen3 21761 ptpjpre1 21783 tx1cn 21821 tx2cn 21822 hausdiag 21857 qustgplem 22332 istdrg2 22389 isngp2 22809 isngp3 22810 isnvc2 22911 isclmp 23304 iscvs 23334 isncvsngp 23356 ovoliunlem1 23706 ismbl2 23731 i1f1lem 23893 i1fres 23909 itg1climres 23918 pilem1 24642 ellogrn 24743 ellogdm 24822 1cubr 25020 atandm 25054 atandm2 25055 atandm3 25056 atandm4 25057 atans2 25109 eldmgm 25200 isfusgrcl 26668 nbgrel 26687 iscusgrvtx 26769 iscusgredg 26771 clwlkclwwlkflem 27386 isph 28249 h2hcau 28408 h2hlm 28409 issh2 28638 isch2 28652 h1dei 28981 elbdop2 29302 dfadj2 29316 cnvadj 29323 hhcno 29335 hhcnf 29336 eleigvec2 29389 riesz2 29497 rnbra 29538 elat2 29771 ofpreima 30030 mpt2mptxf 30043 f1od2 30065 maprnin 30072 xrofsup 30098 xrdifh 30106 cmpcref 30515 ofcfval 30758 ispisys2 30814 1stmbfm 30920 2ndmbfm 30921 eulerpartlems 31020 eulerpartlemgc 31022 eulerpartlemv 31024 eulerpartlemd 31026 eulerpartlemr 31034 eulerpartlemn 31041 ballotlemodife 31158 sgn3da 31202 oddprm2 31335 bnj945 31443 bnj1172 31668 bnj1296 31688 snmlval 31912 eldm3 32245 madeval2 32525 brtxp2 32577 brpprod3a 32582 dffun10 32610 elfuns 32611 brimg 32633 dfrdg4 32647 ellines 32848 opnrebl 32903 bj-ax12ig 33194 bj-equsexval 33228 bj-cleljustab 33422 bj-csbsnlem 33469 bj-mpt2mptALT 33645 bj-elid3 33665 bj-eldiag 33670 taupilem3 33761 topdifinffinlem 33790 relowlssretop 33806 istotbnd3 34178 isbnd2 34190 isbnd3b 34192 exidcl 34283 isdrngo2 34365 isdrngo3 34366 iscrngo2 34404 isdmn2 34462 isfldidl2 34476 isdmn3 34481 brres2 34651 eldmqsres 34667 brxrn2 34749 islshpat 35155 iscvlat2N 35462 ishlat3N 35492 snatpsubN 35888 diclspsn 37332 isnacs2 38211 islnm2 38589 islnr2 38625 islnr3 38626 issdrg2 38709 isdomn3 38723 elinintab 38820 elmapintab 38841 elinlem 38843 cnvcnvintabd 38845 k0004lem1 39383 dffo3f 40269 2reu8 42135 dfdfat2 42151 prproropf1olem0 42423 prprelb 42437 prprspr2 42439 isodd2 42555 iseven5 42583 isodd7 42584 oddprmne2 42631 ismhm0 42802 sgrp2sgrp 42861 0ringdif 42867 isrnghmmul 42890 eliunxp2 43109 mpt2mptx2 43110 elbigo 43342 |
Copyright terms: Public domain | W3C validator |