![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm5.32i | Structured version Visualization version Unicode 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 646 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 213 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: pm5.32ri 648 biadan2 652 anbi2i 705 abai 809 anabs5 823 pm5.33 894 cases 988 equsexvw 1859 equsexv 2077 equsexALT 2142 2sb5rf 2291 2eu8 2400 eq2tri 2523 rexbiia 2900 reubiia 2988 rmobiia 2993 rabbiia 3045 ceqsrexbv 3185 euxfr 3236 2reu5 3260 dfpss3 3531 eldifpr 4002 eldiftp 4027 eldifsn 4110 elrint 4290 elriin 4365 reuxfrd 4642 opeqsn 4714 rabxp 4893 copsex2gb 4967 eliunxp 4994 ressn 5395 dflim2 5502 fncnv 5673 dff1o5 5850 respreima 6037 dff4 6064 dffo3 6065 f1ompt 6072 fsn 6090 fconst3 6158 fconst4 6159 eufnfv 6169 dff13 6189 f1mpt 6192 isocnv3 6253 isores2 6254 isoini 6259 eloprabga 6415 mpt2mptx 6419 resoprab 6424 elrnmpt2res 6442 ov6g 6466 dfwe2 6640 dflim3 6706 dflim4 6707 dfopab2 6879 dfoprab3s 6880 dfoprab3 6881 fparlem1 6928 fparlem2 6929 brtpos2 7010 dftpos3 7022 tpostpos 7024 dfsmo2 7097 dfrecs3 7122 tz7.48-1 7191 ondif1 7234 ondif2 7235 elixp2 7557 mapsnen 7678 xpcomco 7693 eqinf 8031 infempty 8053 r0weon 8474 isinfcard 8554 dfac5lem1 8585 fpwwe 9102 axgroth6 9284 axgroth3 9287 elni2 9333 indpi 9363 recmulnq 9420 genpass 9465 lemul1a 10492 sup3 10599 elnn0z 10984 elznn0 10986 elznn 10987 eluz2b1 11264 eluz2b3 11266 elfz2nn0 11920 elfzo3 11973 shftidt2 13199 clim0 13625 fprod2dlem 14089 divalglem4 14430 ndvdsadd 14444 gcdaddmlem 14547 algfx 14594 isprm3 14688 isprm5 14706 xpsfrnel 15524 isacs2 15614 isfull2 15871 isfth2 15875 tosso 16337 odudlatb 16497 nsgacs 16908 isgim2 16984 isabl2 17493 iscyg3 17576 iscrng2 17851 isdrng2 18040 drngprop 18041 islmim2 18344 islpir2 18530 isnzr2 18542 iunocv 19299 ishil2 19337 islinds2 19426 ssntr 20128 isclo2 20159 isperf2 20223 isperf3 20224 nrmsep3 20426 iscon2 20484 iskgen3 20619 ptpjpre1 20641 tx1cn 20679 tx2cn 20680 hausdiag 20715 qustgplem 21190 istdrg2 21247 isngp2 21666 isngp3 21667 isnvc2 21756 ovoliunlem1 22510 ismbl2 22536 i1f1lem 22703 i1fres 22719 itg1climres 22728 pilem1 23462 ellogrn 23565 ellogdm 23640 1cubr 23824 atandm 23858 atandm2 23859 atandm3 23860 atandm4 23861 atans2 23913 eldmgm 24003 isgrpo2 25981 issubgo 26087 isph 26519 h2hcau 26688 h2hlm 26689 issh2 26918 isch2 26932 h1dei 27259 elbdop2 27580 dfadj2 27594 cnvadj 27601 hhcno 27613 hhcnf 27614 eleigvec2 27667 riesz2 27775 rnbra 27816 elat2 28049 ofpreima 28320 mpt2mptxf 28332 f1od2 28361 maprnin 28368 xrofsup 28405 xrdifh 28414 cmpcref 28728 ofcfval 28970 ispisys2 29026 1stmbfm 29132 2ndmbfm 29133 eulerpartlems 29243 eulerpartlemgc 29245 eulerpartlemv 29247 eulerpartlemd 29249 eulerpartlemr 29257 eulerpartlemn 29264 ballotlemodife 29380 sgn3da 29462 bnj945 29635 bnj1172 29860 bnj1296 29880 snmlval 30104 dfres3 30449 eldm3 30452 nofulllem5 30645 brtxp2 30698 brpprod3a 30703 dffun10 30731 elfuns 30732 brimg 30754 dfrdg4 30768 ellines 30969 opnrebl 31026 bj-ax12ig 31272 bj-equsexval 31297 bj-csbsnlem 31551 bj-mpt2mptALT 31677 bj-elid3 31688 bj-eldiag 31692 taupilem3 31766 topdifinffinlem 31796 relowlssretop 31812 dvtanlemOLD 32037 istotbnd3 32149 isbnd2 32161 isbnd3b 32163 exidcl 32220 isdrngo2 32243 isdrngo3 32244 iscrngo2 32277 isdmn2 32334 isfldidl2 32348 isdmn3 32353 islshpat 32629 iscvlat2N 32936 ishlat3N 32966 snatpsubN 33361 diclspsn 34808 isnacs2 35594 islnm2 35982 islnr2 36019 islnr3 36020 issdrg2 36110 isdomn3 36127 elinintab 36227 elmapintab 36248 elinlem 36250 cnvcnvintabd 36252 isprm7 36705 dffo3f 37504 2reu8 38748 dfdfat2 38768 isodd2 38900 iseven5 38929 isodd7 38930 iscusgrvtx 39635 iscusgredg 39637 ismhm0 40174 sgrp2sgrp 40233 0ringdif 40239 isrnghmmul 40262 eliunxp2 40484 mpt2mptx2 40485 elbigo 40731 |
Copyright terms: Public domain | W3C validator |