![]() |
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 222 | . 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃)) |
4 | 1, 3 | sylan9bb 509 | 1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: rbaibd 540 pw2f1olem 9072 eluz 12833 elicc4 13388 s111 14562 limsupgle 15418 lo1resb 15505 o1resb 15507 isercolllem2 15609 divalgmodcl 16347 ismri2 17575 acsfiel2 17598 eqglact 19096 eqgid 19097 cntzel 19229 dprdsubg 19936 subgdmdprd 19946 dprd2da 19954 dmdprdpr 19961 issubrg3 20492 ishil2 21582 obslbs 21593 iscld2 22854 isperf3 22979 cncnp2 23107 cnnei 23108 trfbas2 23669 flimrest 23809 flfnei 23817 fclsrest 23850 tsmssubm 23969 isnghm2 24563 isnghm3 24564 isnmhm2 24591 iscfil2 25116 caucfil 25133 ellimc2 25728 cnlimc 25739 lhop1 25869 dvfsumlem1 25882 fsumharmonic 26860 fsumvma 27062 fsumvma2 27063 vmasum 27065 chpchtsum 27068 chpub 27069 rpvmasum2 27361 dchrisum0lem1 27365 dirith 27378 uvtx2vtx1edg 29124 uvtx2vtx1edgb 29125 iscplgrnb 29142 frgr3v 29997 adjeu 31611 suppiniseg 32377 suppss3 32418 nndiffz1 32466 islinds5 32949 fsumcvg4 33419 qqhval2lem 33450 indpreima 33512 eulerpartlemf 33858 elorvc 33947 hashreprin 34121 neibastop3 35737 relowlpssretop 36735 sstotbnd2 37132 isbnd3b 37143 lshpkr 38477 isat2 38647 islln4 38868 islpln4 38892 islvol4 38935 islhp2 39358 pw2f1o2val2 42268 rfcnpre1 44192 rfcnpre2 44204 joindm3 47790 meetdm3 47792 catprsc 47821 |
Copyright terms: Public domain | W3C validator |