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 668 | . 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | |
3 | 1, 2 | mpbi 220 | 1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → 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: pm5.32ri 670 biadan2 674 anbi2i 730 abai 836 anabs5 851 pm5.33 922 cases 992 equsexvw 1932 equsexv 2109 equsexALT 2293 2sb5rf 2451 2eu8 2560 eq2tri 2683 rexbiia 3040 reubiia 3127 rmobiia 3132 rabbiia 3185 ceqsrexbv 3337 euxfr 3392 2reu5 3416 dfpss3 3693 eldifpr 4204 eldiftp 4228 eldifsn 4317 elrint 4518 elriin 4593 reuxfrd 4893 opeqsn 4967 rabxp 5154 copsex2gb 5230 eliunxp 5259 dfres3 5403 restidsing 5458 ressn 5671 dflim2 5781 fncnv 5962 dff1o5 6146 respreima 6344 dff4 6373 dffo3 6374 f1ompt 6382 fsn 6402 fconst3 6477 fconst4 6478 eufnfv 6491 dff13 6512 f1mpt 6518 isocnv3 6582 isores2 6583 isoini 6588 eloprabga 6747 mpt2mptx 6751 resoprab 6756 elrnmpt2res 6774 ov6g 6798 dfwe2 6981 dflim3 7047 dflim4 7048 dfopab2 7222 dfoprab3s 7223 dfoprab3 7224 fparlem1 7277 fparlem2 7278 brtpos2 7358 dftpos3 7370 tpostpos 7372 dfsmo2 7444 dfrecs3 7469 tz7.48-1 7538 ondif1 7581 ondif2 7582 elixp2 7912 mapsnen 8035 xpcomco 8050 eqinf 8390 infempty 8412 r0weon 8835 isinfcard 8915 dfac5lem1 8946 fpwwe 9468 axgroth6 9650 axgroth3 9653 elni2 9699 indpi 9729 recmulnq 9786 genpass 9831 lemul1a 10877 sup3 10980 elnn0z 11390 elznn0 11392 elznn 11393 eluz2b1 11759 eluz2b3 11762 elfz2nn0 12431 elfzo3 12486 shftidt2 13821 clim0 14237 fprod2dlem 14710 divalglem4 15119 ndvdsadd 15134 gcdaddmlem 15245 algfx 15293 isprm3 15396 isprm5 15419 isprm7 15420 xpsfrnel 16223 isacs2 16314 isfull2 16571 isfth2 16575 tosso 17036 odudlatb 17196 nsgacs 17630 isgim2 17707 isabl2 18201 iscyg3 18288 iscrng2 18563 isdrng2 18757 drngprop 18758 islmim2 19066 islpir2 19251 isnzr2 19263 iunocv 20025 ishil2 20063 islinds2 20152 ssntr 20862 isclo2 20892 isperf2 20956 isperf3 20957 nrmsep3 21159 isconn2 21217 iskgen3 21352 ptpjpre1 21374 tx1cn 21412 tx2cn 21413 hausdiag 21448 qustgplem 21924 istdrg2 21981 isngp2 22401 isngp3 22402 isnvc2 22503 isclmp 22897 iscvs 22927 isncvsngp 22949 ovoliunlem1 23270 ismbl2 23295 i1f1lem 23456 i1fres 23472 itg1climres 23481 pilem1 24205 ellogrn 24306 ellogdm 24385 1cubr 24569 atandm 24603 atandm2 24604 atandm3 24605 atandm4 24606 atans2 24658 eldmgm 24748 isfusgrcl 26213 iscusgrvtx 26317 iscusgredg 26319 isph 27677 h2hcau 27836 h2hlm 27837 issh2 28066 isch2 28080 h1dei 28409 elbdop2 28730 dfadj2 28744 cnvadj 28751 hhcno 28763 hhcnf 28764 eleigvec2 28817 riesz2 28925 rnbra 28966 elat2 29199 ofpreima 29465 mpt2mptxf 29477 f1od2 29499 maprnin 29506 xrofsup 29533 xrdifh 29542 cmpcref 29917 ofcfval 30160 ispisys2 30216 1stmbfm 30322 2ndmbfm 30323 eulerpartlems 30422 eulerpartlemgc 30424 eulerpartlemv 30426 eulerpartlemd 30428 eulerpartlemr 30436 eulerpartlemn 30443 ballotlemodife 30559 sgn3da 30603 oddprm2 30733 bnj945 30844 bnj1172 31069 bnj1296 31089 snmlval 31313 eldm3 31651 madeval2 31936 brtxp2 31988 brpprod3a 31993 dffun10 32021 elfuns 32022 brimg 32044 dfrdg4 32058 ellines 32259 opnrebl 32315 bj-ax12ig 32615 bj-equsexval 32638 bj-cleljustab 32847 bj-csbsnlem 32898 bj-mpt2mptALT 33072 bj-elid3 33087 bj-eldiag 33091 taupilem3 33165 topdifinffinlem 33195 relowlssretop 33211 istotbnd3 33570 isbnd2 33582 isbnd3b 33584 exidcl 33675 isdrngo2 33757 isdrngo3 33758 iscrngo2 33796 isdmn2 33854 isfldidl2 33868 isdmn3 33873 brres2 34035 eldmqsres 34051 islshpat 34304 iscvlat2N 34611 ishlat3N 34641 snatpsubN 35036 diclspsn 36483 isnacs2 37269 islnm2 37648 islnr2 37684 islnr3 37685 issdrg2 37768 isdomn3 37782 elinintab 37881 elmapintab 37902 elinlem 37904 cnvcnvintabd 37906 k0004lem1 38445 dffo3f 39364 2reu8 41192 dfdfat2 41211 isodd2 41548 iseven5 41576 isodd7 41577 oddprmne2 41624 ismhm0 41805 sgrp2sgrp 41864 0ringdif 41870 isrnghmmul 41893 eliunxp2 42112 mpt2mptx2 42113 elbigo 42345 |
Copyright terms: Public domain | W3C validator |