![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > baibd | Structured version Visualization version GIF version |
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
Ref | Expression |
---|---|
baibd.1 | ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) |
Ref | Expression |
---|---|
baibd | ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | baibd.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | |
2 | ibar 526 | . . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃))) | |
3 | 2 | bicomd 215 | . 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃)) |
4 | 1, 3 | sylan9bb 507 | 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: pw2f1olem 8333 eluz 11982 elicc4 12528 s111 13675 limsupgle 14585 lo1resb 14672 o1resb 14674 isercolllem2 14773 divalgmodcl 15504 ismri2 16645 acsfiel2 16668 issect2 16766 eqglact 17996 eqgid 17997 cntzel 18106 dprdsubg 18777 subgdmdprd 18787 dprd2da 18795 dmdprdpr 18802 issubrg3 19164 ishil2 20426 obslbs 20437 iscld2 21203 isperf3 21328 cncnp2 21456 cnnei 21457 trfbas2 22017 flimrest 22157 flfnei 22165 fclsrest 22198 tsmssubm 22316 isnghm2 22898 isnghm3 22899 isnmhm2 22926 iscfil2 23434 caucfil 23451 ellimc2 24040 cnlimc 24051 lhop1 24176 dvfsumlem1 24188 fsumharmonic 25151 fsumvma 25351 fsumvma2 25352 vmasum 25354 chpchtsum 25357 chpub 25358 rpvmasum2 25614 dchrisum0lem1 25618 dirith 25631 uvtx2vtx1edg 26696 uvtx2vtx1edgb 26697 iscplgrnb 26714 frgr3v 27656 adjeu 29303 suppss3 30050 nndiffz1 30095 fsumcvg4 30541 qqhval2lem 30570 indpreima 30632 eulerpartlemf 30977 elorvc 31067 hashreprin 31247 neibastop3 32895 relowlpssretop 33757 sstotbnd2 34115 isbnd3b 34126 lshpkr 35192 isat2 35362 islln4 35582 islpln4 35606 islvol4 35649 islhp2 36072 pw2f1o2val2 38450 rfcnpre1 39996 rfcnpre2 40008 |
Copyright terms: Public domain | W3C validator |