| 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 528 | . . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃))) | |
| 3 | 2 | bicomd 223 | . 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃)) |
| 4 | 1, 3 | sylan9bb 509 | 1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: rbaibd 540 pw2f1olem 9116 eluz 12892 elicc4 13454 s111 14653 limsupgle 15513 lo1resb 15600 o1resb 15602 isercolllem2 15702 divalgmodcl 16444 ismri2 17675 acsfiel2 17698 eqglact 19197 eqgid 19198 cntzel 19341 dprdsubg 20044 subgdmdprd 20054 dprd2da 20062 dmdprdpr 20069 issubrg3 20600 ishil2 21739 obslbs 21750 iscld2 23036 isperf3 23161 cncnp2 23289 cnnei 23290 trfbas2 23851 flimrest 23991 flfnei 23999 fclsrest 24032 tsmssubm 24151 isnghm2 24745 isnghm3 24746 isnmhm2 24773 iscfil2 25300 caucfil 25317 ellimc2 25912 cnlimc 25923 lhop1 26053 dvfsumlem1 26066 fsumharmonic 27055 fsumvma 27257 fsumvma2 27258 vmasum 27260 chpchtsum 27263 chpub 27264 rpvmasum2 27556 dchrisum0lem1 27560 dirith 27573 uvtx2vtx1edg 29415 uvtx2vtx1edgb 29416 iscplgrnb 29433 frgr3v 30294 adjeu 31908 suppiniseg 32695 suppss3 32735 nndiffz1 32788 indpreima 32850 islinds5 33395 fsumcvg4 33949 qqhval2lem 33982 eulerpartlemf 34372 elorvc 34462 hashreprin 34635 neibastop3 36363 relowlpssretop 37365 sstotbnd2 37781 isbnd3b 37792 lshpkr 39118 isat2 39288 islln4 39509 islpln4 39533 islvol4 39576 islhp2 39999 pw2f1o2val2 43052 modelaxreplem3 44997 rfcnpre1 45024 rfcnpre2 45036 joindm3 48866 meetdm3 48868 catprsc 48902 |
| Copyright terms: Public domain | W3C validator |