![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > baib | Structured version Visualization version GIF version |
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
Ref | Expression |
---|---|
baib.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
baib | ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibar 518 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
2 | baib.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | syl6rbbr 279 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 |
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 383 |
This theorem is referenced by: baibr 526 ceqsrexbv 3487 elrab3 3516 dfpss3 3843 rabsn 4392 elrint2 4653 elpredg 5837 fnres 6147 fvmpti 6423 f1ompt 6524 fliftfun 6705 isocnv3 6725 riotaxfrd 6785 ovid 6924 nlimon 7198 limom 7227 brdifun 7925 xpcomco 8206 0sdomg 8245 f1finf1o 8343 ordtypelem9 8587 isacn 9067 alephinit 9118 isfin5-2 9415 pwfseqlem1 9682 pwfseqlem3 9684 pwfseqlem4 9686 ltresr 10163 xrlenlt 10305 znnnlt1 11606 difrp 12071 elfz 12539 fzolb2 12685 elfzo3 12694 fzouzsplit 12711 rabssnn0fi 12993 caubnd 14306 ello12 14455 elo12 14466 bitsval2 15355 smueqlem 15420 rpexp 15639 ramcl 15940 ismon2 16601 isepi2 16608 isfull2 16778 isfth2 16782 isghm3 17869 gastacos 17950 sylow2alem2 18240 lssnle 18294 isabl2 18408 submcmn2 18451 iscyggen2 18490 iscyg3 18495 cyggexb 18507 gsum2d2 18580 dprdw 18617 dprd2da 18649 iscrng2 18771 dvdsr2 18855 dfrhm2 18927 islmhm3 19241 isdomn2 19514 psrbaglefi 19587 mplsubrglem 19654 prmirredlem 20056 chrnzr 20093 iunocv 20242 iscss2 20247 ishil2 20280 obselocv 20289 bastop1 21018 isclo 21112 maxlp 21172 isperf2 21177 restperf 21209 cnpnei 21289 cnntr 21300 cnprest 21314 cnprest2 21315 lmres 21325 iscnrm2 21363 ist0-2 21369 ist1-2 21372 ishaus2 21376 tgcmp 21425 cmpfi 21432 dfconn2 21443 t1connperf 21460 subislly 21505 tx1cn 21633 tx2cn 21634 xkopt 21679 xkoinjcn 21711 ist0-4 21753 trfil2 21911 fin1aufil 21956 flimtopon 21994 elflim 21995 fclstopon 22036 isfcls2 22037 alexsubALTlem4 22074 ptcmplem3 22078 tgphaus 22140 xmetec 22459 prdsbl 22516 blval2 22587 isnvc2 22723 isnghm2 22748 isnmhm2 22776 0nmhm 22779 xrtgioo 22829 cncfcnvcn 22944 evth 22978 nmhmcn 23139 cmsss 23366 lssbn 23367 srabn 23375 ishl2 23385 ivthlem2 23440 0plef 23659 itg2monolem1 23737 itg2cnlem1 23748 itg2cnlem2 23749 ellimc2 23861 dvne0 23994 ellogdm 24606 dcubic 24794 atans2 24879 amgm 24938 ftalem3 25022 pclogsum 25161 dchrelbas3 25184 lgsabs1 25282 dchrvmaeq0 25414 rpvmasum2 25422 clwwlkwwlksb 27211 ajval 28057 bnsscmcl 28064 axhcompl-zf 28195 seq1hcau 28384 hlim2 28389 issh3 28416 lnopcnre 29238 dmdbr2 29502 elatcv0 29540 iunsnima 29768 1stmbfm 30662 2ndmbfm 30663 eulerpartlemd 30768 oddprm2 31073 cvmlift2lem12 31634 bj-rest10 33373 topdifinfeq 33535 finxpsuclem 33571 curunc 33724 istotbnd2 33901 sstotbnd2 33905 isbnd3b 33916 totbndbnd 33920 ecres2 34387 islnr2 38210 sdrgacs 38297 areaquad 38328 oddm1evenALTV 42114 oddp1evenALTV 42115 |
Copyright terms: Public domain | W3C validator |